|
|
Venues (Conferences, Journals, ...)
|
|
GrowBag graphs for keyword ? (Num. hits/coverage)
Group by:
The graphs summarize 4075 occurrences of 1988 keywords
|
|
|
Results
Found 10042 publication records. Showing 10042 according to the selection in the facets
Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
19 | Kamal Aboul-Hosn |
A Proof-Theoretic Approach to Tactics. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MKM ![In: Mathematical Knowledge Management, 5th International Conference, MKM 2006, Wokingham, UK, August 11-12, 2006, Proceedings, pp. 54-66, 2006, Springer, 3-540-37104-4. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
|
19 | Pedro Quaresma, Predrag Janicic |
Integrating Dynamic Geometry Software, Deduction Systems, and Theorem Repositories. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MKM ![In: Mathematical Knowledge Management, 5th International Conference, MKM 2006, Wokingham, UK, August 11-12, 2006, Proceedings, pp. 280-294, 2006, Springer, 3-540-37104-4. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
|
19 | Matthias Baaz, Stefan Hetzl, Alexander Leitsch, Clemens Richter, Hendrik Spohr |
Proof Transformation by CERES. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MKM ![In: Mathematical Knowledge Management, 5th International Conference, MKM 2006, Wokingham, UK, August 11-12, 2006, Proceedings, pp. 82-93, 2006, Springer, 3-540-37104-4. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
|
19 | Tetsu Iwata, Kaoru Kurosawa |
How to Enhance the Security of the 3GPP Confidentiality and Integrity Algorithms. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FSE ![In: Fast Software Encryption: 12th International Workshop, FSE 2005, Paris, France, February 21-23, 2005, Revised Selected Papers, pp. 268-283, 2005, Springer, 3-540-26541-4. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
|
19 | Ulrich Kohlenbach |
Proof Mining in Functional Analysis. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CiE ![In: New Computational Paradigms, First Conference on Computability in Europe, CiE 2005, Amsterdam, The Netherlands, June 8-12, 2005, Proceedings, pp. 233-234, 2005, Springer, 3-540-26179-6. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
|
19 | Nik Swoboda, Gerard Allwein |
Using DAG transformations to verify Euler/Venn homogeneous and Euler/Venn FOL heterogeneous rules of inference. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Softw. Syst. Model. ![In: Softw. Syst. Model. 3(2), pp. 136-149, 2004. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
Euler and Venn diagrams, Graph transformation, Diagrammatic reasoning, Proof verification |
19 | Michael Soltys, Alasdair Urquhart |
Matrix identities and the pigeonhole principle. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Math. Log. ![In: Arch. Math. Log. 43(3), pp. 351-358, 2004. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
19 | Nadeem Abdul Hamid, Zhong Shao, Valery Trifonov, Stefan Monnier, Zhaozhong Ni |
A Syntactic Approach to Foundational Proof-Carrying Code. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 31(3-4), pp. 191-229, 2003. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
foundational proof-carrying code, syntactic soundness proof, typed assembly language |
19 | Hirotada Kobayashi, Keiji Matsumoto, Tomoyuki Yamakami |
Quantum Merlin-Arthur Proof Systems: Are Multiple Merlins More Helpful to Arthur? ![Search on Bibsonomy](Pics/bibsonomy.png) |
ISAAC ![In: Algorithms and Computation, 14th International Symposium, ISAAC 2003, Kyoto, Japan, December 15-17, 2003, Proceedings, pp. 189-198, 2003, Springer, 3-540-20695-7. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
|
19 | Josh Buresh-Oppenheim, Nicola Galesi, Shlomo Hoory, Avner Magen, Toniann Pitassi |
Rank Bounds and Integrality Gaps for Cutting Planes Procedures Joshua. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FOCS ![In: 44th Symposium on Foundations of Computer Science (FOCS 2003), 11-14 October 2003, Cambridge, MA, USA, Proceedings, pp. 318-327, 2003, IEEE Computer Society, 0-7695-2040-5. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
|
19 | Axel Schairer, Dieter Hutter |
Proof Transformations for Evolutionary Formal Software Development. ![Search on Bibsonomy](Pics/bibsonomy.png) |
AMAST ![In: Algebraic Methodology and Software Technology, 9th International Conference, AMAST 2002, Saint-Gilles-les-Bains, Reunion Island, France, September 9-13, 2002, Proceedings, pp. 441-456, 2002, Springer, 3-540-44144-1. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
|
19 | Ivan Damgård, Eiichiro Fujisaki |
A Statistically-Hiding Integer Commitment Scheme Based on Groups with Hidden Order. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ASIACRYPT ![In: Advances in Cryptology - ASIACRYPT 2002, 8th International Conference on the Theory and Application of Cryptology and Information Security, Queenstown, New Zealand, December 1-5, 2002, Proceedings, pp. 125-142, 2002, Springer, 3-540-00171-9. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
|
19 | Boaz Barak, Yehuda Lindell |
Strict polynomial-time in simulation and extraction. ![Search on Bibsonomy](Pics/bibsonomy.png) |
STOC ![In: Proceedings on 34th Annual ACM Symposium on Theory of Computing, May 19-21, 2002, Montréal, Québec, Canada, pp. 484-493, 2002, ACM, 1-58113-495-9. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
|
19 | Uwe Egly, Hans Tompits |
Proof-complexity results for nonmonotonic reasoning. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACM Trans. Comput. Log. ![In: ACM Trans. Comput. Log. 2(3), pp. 340-387, 2001. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
default logic, circumscription, sequent calculi |
19 | James L. Caldwell |
Extracting General Recursive Program Schemes in Nuprl's Type Theory. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LOPSTR ![In: Logic Based Program Synthesis and Transformation, 11th International Workshop, LOPSTR 2001, Paphos, Cyprus, November 28-30, 2001, Selected Papers, pp. 233-244, 2001, Springer, 3-540-43915-3. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
|
19 | Johan Håstad |
Which NP-Hard Optimization Problems Admit Non-trivial Efficient Approximation Algorithms? ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICALP ![In: Automata, Languages and Programming, 27th International Colloquium, ICALP 2000, Geneva, Switzerland, July 9-15, 2000, Proceedings, pp. 235, 2000, Springer, 3-540-67715-1. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
|
19 | José Espírito Santo |
Revisiting the Correspondence between Cut Elimination and Normalisation. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICALP ![In: Automata, Languages and Programming, 27th International Colloquium, ICALP 2000, Geneva, Switzerland, July 9-15, 2000, Proceedings, pp. 600-611, 2000, Springer, 3-540-67715-1. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
|
19 | Fairouz Kamareddine, François Monin |
On Automating Inductive and Non-inductive Termination Methods. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ASIAN ![In: Advances in Computing Science - ASIAN'99, 5th Asian Computing Science Conference, Phuket, Thailand, December 10-12, 1999, Proceedings, pp. 177-189, 1999, Springer, 3-540-66856-X. The full citation details ...](Pics/full.jpeg) |
1999 |
DBLP DOI BibTeX RDF |
|
19 | Alexander A. Razborov |
Lower Bounds for the Polynomial Calculus. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Comput. Complex. ![In: Comput. Complex. 7(4), pp. 291-324, 1998. The full citation details ...](Pics/full.jpeg) |
1998 |
DBLP DOI BibTeX RDF |
polynomial calculus, Proof complexity, pigeonhole principle |
19 | Myla Archer, Constance L. Heitmeyer |
Human-Style Theorem Proving Using PVS. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 10th International Conference, TPHOLs'97, Murray Hill, NJ, USA, August 19-22, 1997, Proceedings, pp. 33-48, 1997, Springer, 3-540-63379-0. The full citation details ...](Pics/full.jpeg) |
1997 |
DBLP DOI BibTeX RDF |
|
19 | Deepak Kapur, Mahadevan Subramaniam |
Mechanically Verifying a Family of Multiplier Circuits. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CAV ![In: Computer Aided Verification, 8th International Conference, CAV '96, New Brunswick, NJ, USA, July 31 - August 3, 1996, Proceedings, pp. 135-146, 1996, Springer, 3-540-61474-5. The full citation details ...](Pics/full.jpeg) |
1996 |
DBLP DOI BibTeX RDF |
|
19 | Harry Buhrman, Thomas Thierauf |
The Complexity of Generating and Checking Proffs of Membership. ![Search on Bibsonomy](Pics/bibsonomy.png) |
STACS ![In: STACS 96, 13th Annual Symposium on Theoretical Aspects of Computer Science, Grenoble, France, February 22-24, 1996, Proceedings, pp. 75-86, 1996, Springer, 3-540-60922-9. The full citation details ...](Pics/full.jpeg) |
1996 |
DBLP DOI BibTeX RDF |
|
19 | Alberto Coen-Porisini, Richard A. Kemmerer, Dino Mandrioli |
A Formal Framework for ASTRAL Intralevel Proof Obligations. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Trans. Software Eng. ![In: IEEE Trans. Software Eng. 20(8), pp. 548-561, 1994. The full citation details ...](Pics/full.jpeg) |
1994 |
DBLP DOI BibTeX RDF |
intralevel proof obligations, formal software development, mathematical correctness, ASLAN, TRIO, real-time systems, real-time systems, verification, formal specification, formal specification, formal methods, finite state machines, program verification, specification languages, state machines, formal specification language, formal proof, timing requirements, ASTRAL |
19 | Martin Protzen |
Lazy Generation of Induction Hypotheses. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-12, 12th International Conference on Automated Deduction, Nancy, France, June 26 - July 1, 1994, Proceedings, pp. 42-56, 1994, Springer, 3-540-58156-1. The full citation details ...](Pics/full.jpeg) |
1994 |
DBLP DOI BibTeX RDF |
|
19 | Toby Walsh, Alex Nunes, Alan Bundy |
The Use of Proof Plans to Sum Series. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-11, 11th International Conference on Automated Deduction, Saratoga Springs, NY, USA, June 15-18, 1992, Proceedings, pp. 325-339, 1992, Springer, 3-540-55602-8. The full citation details ...](Pics/full.jpeg) |
1992 |
DBLP DOI BibTeX RDF |
|
19 | Seppo Keronen |
Natural Deduction Proof Theory for Logic Programming. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ELP ![In: Extensions of Logic Programming, Third International Workshop, ELP'92, Bologna, Italy, February 26-28, 1992, Proceedings, pp. 265-281, 1992, Springer, 3-540-56454-3. The full citation details ...](Pics/full.jpeg) |
1992 |
DBLP DOI BibTeX RDF |
|
19 | Andrei Voronkov |
On Completeness of Program Synthesis Systems. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CSL ![In: Computer Science Logic, 5th Workshop, CSL '91, Berne, Switzerland, October 7-11, 1991, Proceedings, pp. 411-418, 1991, Springer, 3-540-55789-X. The full citation details ...](Pics/full.jpeg) |
1991 |
DBLP DOI BibTeX RDF |
|
18 | Holger Dell, Dieter van Melkebeek |
Satisfiability allows no nontrivial sparsification unless the polynomial-time hierarchy collapses. ![Search on Bibsonomy](Pics/bibsonomy.png) |
STOC ![In: Proceedings of the 42nd ACM Symposium on Theory of Computing, STOC 2010, Cambridge, Massachusetts, USA, 5-8 June 2010, pp. 251-260, 2010, ACM, 978-1-4503-0050-6. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
arithmetic progression free sets, hereditary graph properties, vertex deletion problems, satisfiability, kernelization, vertex cover, parameterized complexity, probabilistically checkable proofs, feedback vertex set, sparsification |
18 | Jean-François Dufourd |
An Intuitionistic Proof of a Discrete Form of the Jordan Curve Theorem Formalized in Coq with Combinatorial Hypermaps. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 43(1), pp. 19-51, 2009. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
Computer-aided proofs, Coq system, Combinatorial hypermaps, Discrete Jordan Curve Theorem, Formal specifications, Computational topology, Planar subdivisions |
18 | Peter Verdée, Stephan van der Waart van Gulik |
A Generic Framework for Adaptive Vague Logics. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Stud Logica ![In: Stud Logica 90(3), pp. 385-405, 2008. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
supervaluationism, subvaluationism, clarity logic, dynamic proofs, fuzzy logic, vagueness, adaptive logic |
18 | Irene Polycarpou |
Induction as a tool for conceptual coherence in computer science. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACM Southeast Regional Conference ![In: Proceedings of the 46th Annual Southeast Regional Conference, 2008, Auburn, Alabama, USA, March 28-29, 2008, pp. 440-445, 2008, ACM, 978-1-60558-105-7. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
undergraduate computer science curricula, computer science education, structural induction, proofs by induction |
18 | Scott Aaronson, Avi Wigderson |
Algebrization: a new barrier in complexity theory. ![Search on Bibsonomy](Pics/bibsonomy.png) |
STOC ![In: Proceedings of the 40th Annual ACM Symposium on Theory of Computing, Victoria, British Columbia, Canada, May 17-20, 2008, pp. 731-740, 2008, ACM, 978-1-60558-047-0. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
communication complexity, oracles, arithmetization, interactive proofs, query complexity, low-degree polynomials |
18 | Martin Nordio, Peter Müller 0001, Bertrand Meyer 0001 |
Proof-Transforming Compilation of Eiffel Programs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TOOLS (46) ![In: Objects, Components, Models and Patterns, 46th International Conference, TOOLS EUROPE 2008, Zurich, Switzerland, June 30 - July 4, 2008. Proceedings, pp. 316-335, 2008, Springer, 978-3-540-69823-4. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
proof-transforming compiler, CIL, Software verification, Proof-Carrying Code, Eiffel, program proofs |
18 | Dana Moshkovitz, Ran Raz |
Sub-constant error low degree test of almost-linear size. ![Search on Bibsonomy](Pics/bibsonomy.png) |
STOC ![In: Proceedings of the 38th Annual ACM Symposium on Theory of Computing, Seattle, WA, USA, May 21-23, 2006, pp. 21-30, 2006, ACM, 1-59593-134-1. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
plane vs. point test, probabilistically checkable proofs, locally testable codes, low degree testing |
18 | Alex Samorodnitsky, Luca Trevisan |
Gowers uniformity, influence of variables, and PCPs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
STOC ![In: Proceedings of the 38th Annual ACM Symposium on Theory of Computing, Seattle, WA, USA, May 21-23, 2006, pp. 11-20, 2006, ACM, 1-59593-134-1. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
influence of variables, probabilistically checkable proofs, linearity test |
18 | Rafael Pass, Abhi Shelat, Vinod Vaikuntanathan |
Construction of a Non-malleable Encryption Scheme from Any Semantically Secure One. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CRYPTO ![In: Advances in Cryptology - CRYPTO 2006, 26th Annual International Cryptology Conference, Santa Barbara, California, USA, August 20-24, 2006, Proceedings, pp. 271-289, 2006, Springer, 3-540-37432-9. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
Non-interactive Zero-knowledge Proofs, Public-key Encryption, Semantic Security, Non-malleability |
18 | Eli Ben-Sasson, Madhu Sudan 0001 |
Simple PCPs with poly-log rate and query complexity. ![Search on Bibsonomy](Pics/bibsonomy.png) |
STOC ![In: Proceedings of the 37th Annual ACM Symposium on Theory of Computing, Baltimore, MD, USA, May 22-24, 2005, pp. 266-275, 2005, ACM, 1-58113-960-8. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
PCPP, probabilistically checkable proofs, PCP, locally testable codes |
18 | Eli Ben-Sasson, Oded Goldreich 0001, Prahladh Harsha, Madhu Sudan 0001, Salil P. Vadhan |
Robust pcps of proximity, shorter pcps and applications to coding. ![Search on Bibsonomy](Pics/bibsonomy.png) |
STOC ![In: Proceedings of the 36th Annual ACM Symposium on Theory of Computing, Chicago, IL, USA, June 13-16, 2004, pp. 1-10, 2004, ACM, 1-58113-852-0. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
property testing, probabilistically checkable proofs, PCP, locally decodable codes, locally testable codes |
18 | Aggelos Kiayias, Moti Yung |
Non-interactive Zero-Sharing with Applications to Private Distributed Decision Making. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Financial Cryptography ![In: Financial Cryptography, 7th International Conference, FC 2003, Guadeloupe, French West Indies, January 27-30, 2003, Revised Papers, pp. 303-320, 2003, Springer, 3-540-40663-8. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
Veto, Simultaneous Disclosure, Privacy, Electronic Voting, Distributed Decision Making, Proofs of Knowledge |
18 | Bartosz Przydatek, Dawn Xiaodong Song, Adrian Perrig |
SIA: secure information aggregation in sensor networks. ![Search on Bibsonomy](Pics/bibsonomy.png) |
SenSys ![In: Proceedings of the 1st International Conference on Embedded Networked Sensor Systems, SenSys 2003, Los Angeles, California, USA, November 5-7, 2003, pp. 255-265, 2003, ACM, 1-58113-707-9. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
security, sensor networks, approximate, interactive proofs, information aggregation |
18 | Yasuhiko Minamide, Koji Okuma |
Verifying CPS transformations in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MERLIN ![In: Eighth ACM SIGPLAN International Conference on Functional Programming, Workshop on Mechanized reasoning about languages with variable binding, MERLIN 2003, Uppsala, Sweden, August 2003, 2003, ACM, 978-1-58113-800-9. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
program transformation, theorem proving, correctness proofs |
18 | Mihir Bellare, Bennet S. Yee |
Forward-Security in Private-Key Cryptography. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CT-RSA ![In: Topics in Cryptology - CT-RSA 2003, The Cryptographers' Track at the RSA Conference 2003, San Francisco, CA, USA, April 13-17, 2003, Proceedings, pp. 1-18, 2003, Springer, 3-540-00847-0. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
pseudorandom bit generators, message authentication, forward security, Symmetric cryptography, audit logs, proofs of security |
18 | Eli Ben-Sasson, Madhu Sudan 0001, Salil P. Vadhan, Avi Wigderson |
Randomness-efficient low degree tests and short PCPs via epsilon-biased sets. ![Search on Bibsonomy](Pics/bibsonomy.png) |
STOC ![In: Proceedings of the 35th Annual ACM Symposium on Theory of Computing, June 9-11, 2003, San Diego, CA, USA, pp. 612-621, 2003, ACM, 1-58113-674-9. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
property testing, probabilistically checkable proofs, locally testable codes, linearity testing, low degree testing |
18 | Matthias Baaz, Georg Moser |
On Generalizations of Semi-terms of Particularly Simple Form. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CSL ![In: Computer Science Logic, 16th International Workshop, CSL 2002, 11th Annual Conference of the EACSL, Edinburgh, Scotland, UK, September 22-25, 2002, Proceedings, pp. 382-396, 2002, Springer, 3-540-44240-5. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
Structure of Proofs, Complexity of Programs, Proof Theory |
18 | Peter Dybjer, Anton Setzer |
Indexed Induction-Recursion. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Proof Theory in Computer Science ![In: Proof Theory in Computer Science, International Seminar, PTCS 2001, Dagstuhl Castle, Germany, October 7-12, 2001, Proceedings, pp. 93-113, 2001, Springer, 3-540-42752-X. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
Dependent type theory, Martin-Löf Type Theory, inductive-recursive definitions, inductive families, normalization proofs, generic programming, inductive definitions, initial algebras |
18 | Dan Grossman, J. Gregory Morrisett, Steve Zdancewic |
Syntactic type abstraction. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACM Trans. Program. Lang. Syst. ![In: ACM Trans. Program. Lang. Syst. 22(6), pp. 1037-1080, 2000. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
proof techniques, syntactic proofs, type abstraction, operational semantics, parametricity |
18 | Adam L. Young, Moti Yung |
Towards Signature-Only Signature Schemes. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ASIACRYPT ![In: Advances in Cryptology - ASIACRYPT 2000, 6th International Conference on the Theory and Application of Cryptology and Information Security, Kyoto, Japan, December 3-7, 2000, Proceedings, pp. 97-115, 2000, Springer, 3-540-41404-5. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
Public Key Cryptosystems (PKCS), nested trapdoor, abuse freeness, (subliminal) leakage, design validation proofs, FIPS, digital signature, decryption, Public Key Infrastructure (PKI), NIST |
18 | Anna Gál, Shai Halevi, Richard J. Lipton, Erez Petrank |
Computing from Partial Solutions. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CCC ![In: Proceedings of the 14th Annual IEEE Conference on Computational Complexity, Atlanta, Georgia, USA, May 4-6, 1999, pp. 34-45, 1999, IEEE Computer Society, 0-7695-0075-7. The full citation details ...](Pics/full.jpeg) |
1999 |
DBLP DOI BibTeX RDF |
Robust proofs, erasure correction, erasure-resilient reductions, fault tolerant computations, NP-Hardness |
18 | Gerrit Bleumer |
Biometric yet Privacy Protecting Person Authentication. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Information Hiding ![In: Information Hiding, Second International Workshop, Portland, Oregon, USA, April 14-17, 1998, Proceedings, pp. 99-110, 1998, Springer, 3-540-65386-4. The full citation details ...](Pics/full.jpeg) |
1998 |
DBLP DOI BibTeX RDF |
Non-transferable certificates, Wallets-with-observer, Biometric person authentication, Blind Signatures, Interactive proofs |
18 | Farokh B. Bastani, Bojan Cukic |
Impact of program transformation on software reliability assessment. ![Search on Bibsonomy](Pics/bibsonomy.png) |
HASE ![In: 1st High-Assurance Systems Engineering Workshop (HASE '96), October 22, 1996, Niagara, Canada, Proceedings, pp. 214-221, 1996, IEEE Computer Society, 0-8186-7629-9. The full citation details ...](Pics/full.jpeg) |
1996 |
DBLP DOI BibTeX RDF |
statistical sampling method, complete program paths, partial proofs, reliability assessment procedure, formal methods, program transformation, program verification, correctness, software fault tolerance, safety critical software, test cases, operational profile, reliability estimate, software reliability assessment |
18 | Mats Per Erik Heimdahl, Barbara J. Czerny |
Using PVS to analyze hierarchical state-based requirements for completeness and consistency. ![Search on Bibsonomy](Pics/bibsonomy.png) |
HASE ![In: 1st High-Assurance Systems Engineering Workshop (HASE '96), October 22, 1996, Niagara, Canada, Proceedings, pp. 252-262, 1996, IEEE Computer Society, 0-8186-7629-9. The full citation details ...](Pics/full.jpeg) |
1996 |
DBLP DOI BibTeX RDF |
hierarchical state based requirements specifications, input sequence, analysis procedures, large real world requirements specification, hierarchical state based language, Requirements State Machine Language, Prototype Verification System, theorem proving component, spurious error reports, formal specifications, robustness, consistency, program verification, completeness, Binary Decision Diagrams, BDDs, PVS, interactive environment, formal proofs, RSML |
18 | Souâd Taouil-Traverson, Sylvie Vignes |
Preliminary Analysis Cycle for B-Method Software Development. ![Search on Bibsonomy](Pics/bibsonomy.png) |
EUROMICRO ![In: 22rd EUROMICRO Conference '96, Beyond 2000: Hardware and Software Design Strategies, September 2-5, 1996, Prague, Czech Republic, pp. 319-, 1996, IEEE Computer Society, 0-8186-7487-3. The full citation details ...](Pics/full.jpeg) |
1996 |
DBLP DOI BibTeX RDF |
preliminary analysis cycle, B-method software development, a priori errors detection, inconsistency deficiencies, formal specification, formal specifications, formal methods, correctness proofs, incompleteness, testing process, software life-cycle |
18 | Uriel Feige, Joe Kilian |
Zero Knowledge and the Chromatic Number. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CCC ![In: Proceedings of the Eleveth Annual IEEE Conference on Computational Complexity, Philadelphia, Pennsylvania, USA, May 24-27, 1996, pp. 278-287, 1996, IEEE Computer Society, 0-8186-7386-9. The full citation details ...](Pics/full.jpeg) |
1996 |
DBLP DOI BibTeX RDF |
approximation algorithms, zero knowledge, chromatic number, probabilistically checkable proofs |
18 | Ramayya Kumar, Thomas Kropf, Klaus Schneider 0001 |
Formal synthesis of circuits with a simple handshake protocol. ![Search on Bibsonomy](Pics/bibsonomy.png) |
VLSI Design ![In: 8th International Conference on VLSI Design (VLSI Design 1995), 4-7 January 1995, New Delhi, India, pp. 255-259, 1995, IEEE Computer Society, 0-8186-6905-5. The full citation details ...](Pics/full.jpeg) |
1995 |
DBLP DOI BibTeX RDF |
formal circuit synthesis, preproven building blocks, higher-order temporal operators, parametrized data signals, sequentially composed modules, parallel module composition, protocols, high level synthesis, logic design, operator semantics, template, formal logic, correctness proofs, synchronous circuits, handshake protocol, HOL theorem prover |
18 | Bruce W. Weide, Stephen H. Edwards, Douglas E. Harms, David Alex Lamb |
Design and Specification of Iterators Using the Swapping Paradigm. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Trans. Software Eng. ![In: IEEE Trans. Software Eng. 20(8), pp. 631-643, 1994. The full citation details ...](Pics/full.jpeg) |
1994 |
DBLP DOI BibTeX RDF |
swapping paradigm, common interface model, user defined iterator abstractions, modular correctness proofs, formal specification, formal specification, formal methods, program verification, program verification, iterators, iterator designs, swapping, proof of correctness, modular reasoning, data encapsulation, imperative languages |
18 | Josyula R. Rao |
Reasoning about Probabilistic Parallel Programs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACM Trans. Program. Lang. Syst. ![In: ACM Trans. Program. Lang. Syst. 16(3), pp. 798-842, 1994. The full citation details ...](Pics/full.jpeg) |
1994 |
DBLP DOI BibTeX RDF |
verification, parallel programming, probabilistic algorithms, correctness proofs, programming methodology, specification techniques |
18 | Matthias Anlauff, Stefan Jähnichen, Martin Simons 0001 |
An experimental support system for formal mathematical reasoning. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FME ![In: FME '94: Industrial Benefit of Formal Methods, Second International Symposium of Formal Methods Europe, Barcelona, Spain, October 24-18, 1994, Proceedings, pp. 421-440, 1994, Springer, 3-540-58555-9. The full citation details ...](Pics/full.jpeg) |
1994 |
DBLP DOI BibTeX RDF |
tool support, proofs, logical frameworks, formal reasoning |
18 | Mark G. Staskauskas |
Formal Derivation of Concurrent Programs: An Example from Industry. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Trans. Software Eng. ![In: IEEE Trans. Software Eng. 19(5), pp. 503-528, 1993. The full citation details ...](Pics/full.jpeg) |
1993 |
DBLP DOI BibTeX RDF |
tapes, I/O channels, UNITY methodology, resource allocation algorithm, formal specification, parallel programming, specifications, operating system, program verification, concurrent programs, proofs, disks, formal derivation, I/O subsystem |
18 | Flemming Nielson, Hanne Riis Nielson |
Layered Predicates. ![Search on Bibsonomy](Pics/bibsonomy.png) |
REX Workshop ![In: Sematics: Foundations and Applications, REX Workshop, Beekbergen, The Netherlands, June 1-4, 1992, Proceedings, pp. 425-456, 1992, Springer, 3-540-56596-5. The full citation details ...](Pics/full.jpeg) |
1992 |
DBLP DOI BibTeX RDF |
partial equivalence relations, Kripke-logical relations, layered predicates, Kripke-layered predicates, substitution properties, well-structured proofs, correctness of code generation, proof principles, denotational semantics, logical relations |
18 | Laura K. Dillon |
Verifying General Safety Properties of Ada Tasking Programs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Trans. Software Eng. ![In: IEEE Trans. Software Eng. 16(1), pp. 51-63, 1990. The full citation details ...](Pics/full.jpeg) |
1990 |
DBLP DOI BibTeX RDF |
safety properties verification, Ada tasking programs, isolation approach, automating partial correctness proofs, Ada, program verification, concurrent programs, deadlock, mutual exclusion, symbolic execution, multiprocessing programs |
18 | Dipankar Sarkar 0001, S. C. De Sarkar |
A Theorem Prover for Verifying Iterative Programs Over Integers. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Trans. Software Eng. ![In: IEEE Trans. Software Eng. 15(12), pp. 1550-1566, 1989. The full citation details ...](Pics/full.jpeg) |
1989 |
DBLP DOI BibTeX RDF |
rule-based theorem prover, iterative programs, overall proof construction strategy, array-sorting program, expert systems, theorem proving, program verification, performance measures, iterative methods, correctness proofs |
18 | R. Geoff Dromey |
Systematic Program Development. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Trans. Software Eng. ![In: IEEE Trans. Software Eng. 14(1), pp. 12-29, 1988. The full citation details ...](Pics/full.jpeg) |
1988 |
DBLP DOI BibTeX RDF |
goal-oriented programming, case analysis, constructive program proofs, software engineering, data structure, refinements, programming, program development, problem decomposition, program structure, postcondition |
18 | Louis C. Guillou, Jean-Jacques Quisquater |
A "Paradoxical" Indentity-Based Signature Scheme Resulting from Zero-Knowledge. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CRYPTO ![In: Advances in Cryptology - CRYPTO '88, 8th Annual International Cryptology Conference, Santa Barbara, California, USA, August 21-25, 1988, Proceedings, pp. 216-231, 1988, Springer, 3-540-97196-3. The full citation details ...](Pics/full.jpeg) |
1988 |
DBLP DOI BibTeX RDF |
zero-knowledge interactive proofs, identity-based system, public key system, complexity, authentication, integrity, digital signature, randomization, identification, factoring, cryptology |
18 | C. A. R. Hoare |
An Axiomatic Basis for Computer Programming. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Commun. ACM ![In: Commun. ACM 12(10), pp. 576-580, 1969. The full citation details ...](Pics/full.jpeg) |
1969 |
DBLP DOI BibTeX RDF |
axiomatic method, formal language definition, machine-independent programming, program documentation, theory of programming' proofs of programs, programming language design |
15 | Jakob Schulz, Emin Karayel |
Karatsuba Multiplication on Integers. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2024, 2024. The full citation details ...](Pics/full.jpeg) |
2024 |
DBLP BibTeX RDF |
|
15 | Axel Bergström, Tjark Weber |
Verified QBF Solving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2024, 2024. The full citation details ...](Pics/full.jpeg) |
2024 |
DBLP BibTeX RDF |
|
15 | Palle Raabjerg, Johannes Åman Pohjola, Tjark Weber |
Broadcast Psi-calculi. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2024, 2024. The full citation details ...](Pics/full.jpeg) |
2024 |
DBLP BibTeX RDF |
|
15 | Ata Keskin |
Doob's Upcrossing Inequality and Martingale Convergence Theorem. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2024, 2024. The full citation details ...](Pics/full.jpeg) |
2024 |
DBLP BibTeX RDF |
|
15 | Terru Stübinger, Lars Hupel |
Go Code Generation for Isabelle. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2024, 2024. The full citation details ...](Pics/full.jpeg) |
2024 |
DBLP BibTeX RDF |
|
15 | Azucena Garvía Bosshard, Christoph Sprenger 0001, Jonathan Bootle |
The Sumcheck Protocol. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2024, 2024. The full citation details ...](Pics/full.jpeg) |
2024 |
DBLP BibTeX RDF |
|
15 | Tobias Nipkow |
Region Quadtrees. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2024, 2024. The full citation details ...](Pics/full.jpeg) |
2024 |
DBLP BibTeX RDF |
|
15 | Manuel Eberl |
Kummer's congruence. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2024, 2024. The full citation details ...](Pics/full.jpeg) |
2024 |
DBLP BibTeX RDF |
|
15 | Sebastián Buss |
Decomposition of totally ordered hoops. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2024, 2024. The full citation details ...](Pics/full.jpeg) |
2024 |
DBLP BibTeX RDF |
|
15 | Manuel Eberl |
Continued Fractions. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2024, 2024. The full citation details ...](Pics/full.jpeg) |
2024 |
DBLP BibTeX RDF |
|
15 | Georg Struth, Tanguy Massacrier |
Cubical Categories. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2024, 2024. The full citation details ...](Pics/full.jpeg) |
2024 |
DBLP BibTeX RDF |
|
15 | Peter Gammie |
ConcurrentHOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2024, 2024. The full citation details ...](Pics/full.jpeg) |
2024 |
DBLP BibTeX RDF |
|
15 | Xavier Parent, Christoph Benzmüller |
Conditional normative reasoning as a fragment of HOL (Isabelle/HOL dataset). ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2024, 2024. The full citation details ...](Pics/full.jpeg) |
2024 |
DBLP BibTeX RDF |
|
15 | Achim D. Brucker, Amy Stell |
(Extended) Interval Analysis. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2024, 2024. The full citation details ...](Pics/full.jpeg) |
2024 |
DBLP BibTeX RDF |
|
15 | Pasquale Noce |
Information Flow Control via Stateful Intransitive Noninterference in Language IMP. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2024, 2024. The full citation details ...](Pics/full.jpeg) |
2024 |
DBLP BibTeX RDF |
|
15 | Jamie Chen |
Wieferich-Kempner Theorem. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2024, 2024. The full citation details ...](Pics/full.jpeg) |
2024 |
DBLP BibTeX RDF |
|
15 | Cameron Calk, Georg Struth |
Higher Globular Catoids and Quantales. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2024, 2024. The full citation details ...](Pics/full.jpeg) |
2024 |
DBLP BibTeX RDF |
|
15 | Alexander Treml |
Uncertainty Principle. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2024, 2024. The full citation details ...](Pics/full.jpeg) |
2024 |
DBLP BibTeX RDF |
|
15 | Yong Kiam Tan, Jiong Yang |
Approximate Model Counting. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2024, 2024. The full citation details ...](Pics/full.jpeg) |
2024 |
DBLP BibTeX RDF |
|
15 | Anders Schlichtkrull |
Soundness of the Q0 proof system for higher-order logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2023, 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP BibTeX RDF |
|
15 | Chelsea Edmonds |
General Probabilistic Techniques for Combinatorics and the Lovasz Local Lemma. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2023, 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP BibTeX RDF |
|
15 | Katharina Kreuzer, Manuel Eberl |
Elimination of Repeated Factors Algorithm. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2023, 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP BibTeX RDF |
|
15 | Emin Karayel |
Distributed Distinct Elements. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2023, 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP BibTeX RDF |
|
15 | Emin Karayel |
Expander Graphs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2023, 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP BibTeX RDF |
|
15 | Anton Danilkin, Loïc Chevalier |
Three Squares Theorem. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2023, 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP BibTeX RDF |
|
15 | Benjamin Bisping, Luisa Montanari |
Coupled Similarity and Contrasimilarity, and How to Compute Them. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2023, 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP BibTeX RDF |
|
15 | Cárolos Laméris |
Myhill-Nerode Theorem for Nominal G-Automata. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2023, 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP BibTeX RDF |
|
15 | Chelsea Edmonds, Lawrence C. Paulson |
Hypergraph Colouring Bounds. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2023, 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP BibTeX RDF |
|
15 | Manuel Eberl |
Lambert Series. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2023, 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP BibTeX RDF |
|
15 | Anthony Bordg, Adrián Doña Mateo |
Strict Omega Categories. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2023, 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP BibTeX RDF |
|
15 | Ata Keskin |
Eudoxus Reals. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2023, 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP BibTeX RDF |
|
15 | Frank J. Balbach |
The Cook-Levin theorem. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2023, 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP BibTeX RDF |
|
15 | Andrei Popescu 0001 |
Renaming-Enriched Sets (Rensets) and Renaming-Based Recursion. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2023, 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP BibTeX RDF |
|
15 | Mathias Schack Rabing |
Ceva's Theorem. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2023, 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP BibTeX RDF |
|
15 | Maximilian Spitz |
Gray Codes for Arbitrary Numeral Systems. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2023, 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP BibTeX RDF |
|
15 | Rodrigo Raya |
Group Law of Edwards Elliptic Curves. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2023, 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP BibTeX RDF |
|
Displaying result #501 - #600 of 10042 (100 per page; Change: ) Pages: [ <<][ 1][ 2][ 3][ 4][ 5][ 6][ 7][ 8][ 9][ 10][ 11][ 12][ 13][ 14][ 15][ >>] |
|