Search results for "proofs"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
24	Kim-Kwang Raymond Choo	Refuting Security Proofs for Tripartite Key Exchange with Model Checker in Planning Problem Setting.	CSFW	2006	DBLP DOI BibTeX RDF
24	Toni Jussila, Carsten Sinz, Armin Biere	Extended Resolution Proofs for Symbolic SAT Solving with Quantification.	SAT	2006	DBLP DOI BibTeX RDF
24	Chad E. Brown	Verifying and Invalidating Textbook Proofs Using Scunak.	MKM	2006	DBLP DOI BibTeX RDF
24	Wilfried Sieg, Saverio Cittadini	Normal Natural Deduction Proofs (in Non-classical Logics).	Mechanizing Mathematical Reasoning	2005	DBLP DOI BibTeX RDF
24	Craig Gentry, David Molnar, Zulfikar Ramzan	Efficient Designated Confirmer Signatures Without Random Oracles or General Zero-Knowledge Proofs.	ASIACRYPT	2005	DBLP DOI BibTeX RDF
24	Endre Bangerter, Jan Camenisch, Ueli M. Maurer	Efficient Proofs of Knowledge of Discrete Logarithms and Representations in Groups with Hidden Order.	Public Key Cryptography	2005	DBLP DOI BibTeX RDF
24	L. Darrell Whitley, Jonathan E. Rowe	Gray, Binary and Real Valued Encodings: Quad Search and Locality Proofs.	FOGA	2005	DBLP DOI BibTeX RDF
24	Marc Fischlin	Communication-Efficient Non-interactive Proofs of Knowledge with Online Extractors.	CRYPTO	2005	DBLP DOI BibTeX RDF
24	Jean Flower, Judith Masthoff, Gem Stapleton	Generating Readable Proofs: A Heuristic Approach to Theorem Proving With Spider Diagrams.	Diagrams	2004	DBLP DOI BibTeX RDF
24	Rafail Ostrovsky, Charles Rackoff, Adam D. Smith	Efficient Consistency Proofs for Generalized Queries on a Committed Database.	ICALP	2004	DBLP DOI BibTeX RDF
24	Ivan Damgård, Serge Fehr, Louis Salvail	Zero-Knowledge Proofs and String Commitments Withstanding Quantum Attacks.	CRYPTO	2004	DBLP DOI BibTeX RDF
24	Ran Raz, Amir Shpilka	On the Power of Quantum Proofs.	CCC	2004	DBLP DOI BibTeX RDF
24	Dima Grigoriev, Edward A. Hirsch, Dmitrii V. Pasechnik	Complexity of Semi-algebraic Proofs.	STACS	2002	DBLP DOI BibTeX RDF
24	David McMath, Marianna Rozenfeld, Richard Sommer	A Computer Environment for Writing Ordinary Mathematical Proofs.	LPAR	2001	DBLP DOI BibTeX RDF
24	Uwe Egly, Stephan Schmitt	Deriving Modular Programs from Short Proofs.	IJCAR	2001	DBLP DOI BibTeX RDF
24	Iman Poernomo, John N. Crossley	Protocols between Programs and Proofs.	LOPSTR (LNCS 2042: Selected Papers)	2000	DBLP DOI BibTeX RDF
24	Olga Caprotti, Martijn Oostdijk	On Communicating Proofs in Interactive Mathematical Documents.	AISC	2000	DBLP DOI BibTeX RDF
24	Jose L. Cordova	Mathematical proofs as graph search problems in theory courses.	SIGCSE	1999	DBLP DOI BibTeX RDF
24	Helmut Horacek	Presenting Proofs in a Human-Oriented Way.	CADE	1999	DBLP DOI BibTeX RDF
24	Ransom Richardson, Joe Kilian	On the Concurrent Composition of Zero-Knowledge Proofs.	EUROCRYPT	1999	DBLP DOI BibTeX RDF	Asynchronous Attacks, Black-box Simulation, Zero Knowledge
24	Peter Nordin, Anders Eriksson, Mats G. Nordahl	Genetic Reasoning: Evolutionary Induction of Mathematical Proofs.	EuroGP	1999	DBLP DOI BibTeX RDF
24	Erica Melis, Axel Schairer	Similarities and Reuse of Proofs in Formal Software Verification.	EWCBR	1998	DBLP DOI BibTeX RDF
24	Michael Beeson	Automatic Generation of Epsilon-Delta Proofs of Continuity.	AISC	1998	DBLP DOI BibTeX RDF
24	Tobias Nipkow	More Church-Rosser Proofs (in Isabelle/HOL).	CADE	1996	DBLP DOI BibTeX RDF
24	Xiaorong Huang, Armin Fiedler	Presenting Machine-Found Proofs.	CADE	1996	DBLP DOI BibTeX RDF
24	Joan Boyar, René Peralta 0001	Short Discrete Proofs.	EUROCRYPT	1996	DBLP DOI BibTeX RDF
24	Adel Bouhoula	SPIKE: a System for Sufficient Completeness and Parameterized Inductive Proofs.	CADE	1994	DBLP DOI BibTeX RDF
24	Dieter Hutter	Synthesis of Induction Orderings for Existence Proofs.	CADE	1994	DBLP DOI BibTeX RDF
24	Lidong Chen, Ivan Damgård, Torben P. Pedersen	Parallel Divertibility of Proofs of Knowledge (Extended Abstract).	EUROCRYPT	1994	DBLP DOI BibTeX RDF
24	Pavel Pudlák, Samuel R. Buss	How to Lie Without Being (Easily) Convicted and the Length of Proofs in Propositional Calculus.	CSL	1994	DBLP DOI BibTeX RDF
24	Ricardo Caferra, Michel Herment	GLEFATINF: A Graphic Framework for Combining Theorem Provers and Editing Proofs for Different Logics.	DISCO	1993	DBLP DOI BibTeX RDF	Graphic Proof Presentation, Proof Edition, Logical Frameworks
24	Thomas M. Niermann, Wu-Tung Cheng, Janak H. Patel	PROOFS: a fast, memory-efficient sequential circuit fault simulator.	IEEE Trans. Comput. Aided Des. Integr. Circuits Syst.	1992	DBLP DOI BibTeX RDF
24	Alfredo De Santis, Giuseppe Persiano, Moti Yung	One-Message Statistical Zero-Knowledge Proofs and Space-Bounded Verifier.	ICALP	1992	DBLP DOI BibTeX RDF
24	Tatsuaki Okamoto, David Chaum, Kazuo Ohta	Direct Zero Knowledge Proofs of Computational Power in Five Rounds.	EUROCRYPT	1991	DBLP DOI BibTeX RDF
24	Mihir Bellare, Shafi Goldwasser	New Paradigms for Digital Signatures and Message Authentication Based on Non-Interative Zero Knowledge Proofs.	CRYPTO	1989	DBLP DOI BibTeX RDF
24	Joe Kilian, Silvio Micali, Rafail Ostrovsky	Minimum Resource Zero-Knowledge Proofs (Extended Abstract).	CRYPTO	1989	DBLP DOI BibTeX RDF
24	Michel Parigot	Programming with Proofs: A Second Order Type Theory.	ESOP	1988	DBLP DOI BibTeX RDF
24	Christoph Walther	Argument-Bounded Algorithms as a Basis for Automated Termination Proofs.	CADE	1988	DBLP DOI BibTeX RDF
24	Donald Simon	Checking Natural Language Proofs.	CADE	1988	DBLP DOI BibTeX RDF
24	Ketan Mulmuley	The Mechanization of Existence Proofs of Recursive Predicates.	CADE	1984	DBLP DOI BibTeX RDF
24	Frank Pfenning	Analytic and Non-analytic Proofs.	CADE	1984	DBLP DOI BibTeX RDF
24	Chris Goad	Proofs as Description of Computation.	CADE	1980	DBLP DOI BibTeX RDF
24	Adam Chlipala	A verified compiler for an impure functional language.	POPL	2010	DBLP DOI BibTeX RDF	compiler verification, interactive proof assistants
24	Eugene Goldberg	Boundary Points and Resolution.	SAT	2009	DBLP DOI BibTeX RDF	proof quality, resolution, SAT-solver, boundary points
24	Avik Chaudhuri, Deepak Garg 0001	PCAL: Language Support for Proof-Carrying Authorization Systems.	ESORICS	2009	DBLP DOI BibTeX RDF
24	Santiago Zanella Béguelin, Gilles Barthe, Benjamin Grégoire, Federico Olmedo	Formally Certifying the Security of Digital Signature Schemes.	SP	2009	DBLP DOI BibTeX RDF
24	Gianpiero Cabodi, Paolo Camurati, Marco Murciano	Automated abstraction by incremental refinement in interpolant-based model checking.	ICCAD	2008	DBLP DOI BibTeX RDF
24	Reynald Affeldt, Miki Tanaka, Nicolas Marti	Formal Proof of Provable Security by Game-Playing in a Proof Assistant.	ProvSec	2007	DBLP DOI BibTeX RDF
24	Iman Poernomo	Synthesis of Data Views for Communicating Processes.	LOPSTR	2007	DBLP DOI BibTeX RDF
24	Giovanni Di Crescenzo	You Can Prove So Many Things in Zero-Knowledge.	CISC	2005	DBLP DOI BibTeX RDF
24	Peter B. Andrews	Some Reflections on Proof Transformations.	Mechanizing Mathematical Reasoning	2005	DBLP DOI BibTeX RDF
24	Venkatesh Choppella, Christopher T. Haynes	Source-Tracking Unification.	CADE	2003	DBLP DOI BibTeX RDF
24	Maria Luisa Bonet, Nicola Galesi	A Study of Proof Search Algorithms for Resolution and Polynomial Calculus.	FOCS	1999	DBLP DOI BibTeX RDF
24	Chia-Chu Chiang, Joseph E. Urban	Validating Software Specifications against User Claims.	COMPSAC	1999	DBLP DOI BibTeX RDF
24	Kenneth L. McMillan	Minimalist Proof Assistants: Interactions of Technology and Methodology in Formal System Level Verification (abstract).	FMCAD	1998	DBLP DOI BibTeX RDF
24	Victor L. Winter, James M. Boyle	Proving refinement transformations for deriving high-assurance software.	HASE	1996	DBLP DOI BibTeX RDF	refinement transformation proving, high-assurance software engineering, refinement-based approach, TAMPR transformation system, automated refinement, semantic framework, automated reasoning system, software engineering, program transformations, program verification, stepwise refinement, high-level specification
24	Marta Franová	Automated Inductive Reasoning as a Support of Deductive Reasoning in a User-Independent Automation of Inductive Theorem Proving.	ISMIS	1996	DBLP DOI BibTeX RDF
24	Robert Harper 0001, Furio Honsell, Gordon D. Plotkin	A Framework for Defining Logics.	J. ACM	1993	DBLP DOI BibTeX RDF	proof checking, interactive theorem proving, typed lambda calculus, formal systems
24	Hubert Bertling, Harald Ganzinger	Completion-Time Optimization of Rewrite-Time Goal Solving.	RTA	1989	DBLP DOI BibTeX RDF
23	Jorge F. Salas	A Language for Encoding and Reconstruction of Rewriting Proofs.	SCCC	2009	DBLP DOI BibTeX RDF	Semiautomated theorem proving, encoding languages for proofs, rewriting induction, rewriting systems
23	Petr Hájek 0001	Ontological Proofs of Existence and Non-Existence.	Stud Logica	2008	DBLP DOI BibTeX RDF	ontological proofs, non-existence, Gödel, Caramuel, existence
23	Jean Goubault-Larrecq	Towards Producing Formally Checkable Security Proofs, Automatically.	CSF	2008	DBLP DOI BibTeX RDF	Dolev-Yao model, h1, security, model-checking, first-order logic, tree automata, proofs, Coq, Paradox
23	Harry Halpin	From Typed-Functional Semantic Web Services to Proofs.	ISWC	2006	DBLP DOI BibTeX RDF	Functional Programming, Semantic Web Services, Type Theory, Proofs, Curry-Howard Isomorphism
23	Marc Shapiro 0001	Practical proofs of concurrent programs.	ICFP	2006	DBLP DOI BibTeX RDF	concurrent programming, assertions, hoare logic, program proofs, rely-guarantee
23	Sorin Lerner, Todd D. Millstein, Erika Rice, Craig Chambers	Automated soundness proofs for dataflow analyses and transformations via local rules.	POPL	2005	DBLP DOI BibTeX RDF	automated correctness proofs, compiler optimization
23	Sultan Almuhammadi, Clifford Neuman	Security and Privacy Using One-Round Zero-Knowledge Proofs.	CEC	2005	DBLP DOI BibTeX RDF	privacy, e-commerce, computer security, public-key cryptography, trusted computing, identity theft, Zero-knowledge proofs
23	Manuel Kauers	Computer proofs for polynomial identities in arbitrary many variables.	ISSAC	2004	DBLP DOI BibTeX RDF	computer proofs, polynomial identities
23	Dieter Hofbauer	Termination Proofs for Ground Rewrite Systems - Interpretations and Derivational Complexity.	Appl. Algebra Eng. Commun. Comput.	2001	DBLP DOI BibTeX RDF	Ground rewriting, Termination proofs, Derivational complexity, Term rewriting systems
23	Salil P. Vadhan	On transformation of interactive proofs that preserve the prover's complexity.	STOC	2000	DBLP DOI BibTeX RDF	zero-knowledge proofs, interactive proof systems, Arthur-Merlin games, pseudorandom permutations
23	Khanh Quoc Nguyen, Vijay Varadharajan, Yi Mu 0001	Batching Proofs of Knowledge and Its Applications.	DEXA Workshops	1999	DBLP DOI BibTeX RDF	Incremental Cryptography, Efficient Protocols, Electronic Cash, Proofs of Knowledge
23	Víctor M. Gulías, J. Santiago Jorge, Juan J. Quintela, José Luis Freire	From Sequential to Distributed Formal Proofs.	EUROCAST	1997	DBLP DOI BibTeX RDF	Distributed Computing, Functional Programming, Formal Proofs
23	Paolo Volpe	Abstractions of Uniform Proofs.	ALP	1996	DBLP DOI BibTeX RDF	uniform proofs, inference rule systems, abstract interpretation
23	Kenneth W. Regan, D. Sivakumar, Jin-yi Cai	Pseudorandom Generators, Measure Theory, and Natural Proofs.	FOCS	1995	DBLP DOI BibTeX RDF	natural proofs, resource-bounded measure theory, partial converse, computational complexity, theorem proving, formal languages, random number generation, measure theory, pseudorandom number generators
23	Silvio Micali	CS Proofs (Extended Abstracts)	FOCS	1994	DBLP DOI BibTeX RDF	computationally sound proof, CS proofs, computationally-based notion, cryptographic assumption, computational complexity, NP complete problem, polynomial time, proof, random oracle
23	Paul Beame, Russell Impagliazzo, Jan Krajícek, Toniann Pitassi, Pavel Pudlák	Lower Bound on Hilbert's Nullstellensatz and propositional proofs	FOCS	1994	DBLP DOI BibTeX RDF	propositional formulas, Hilbert's Nullstellensatz, propositional proofs, modular counting principle, fixed cardinality, algebraic equations
23	Sanjeev Arora, Shmuel Safra	Probabilistic Checking of Proofs; A New Characterization of NP	FOCS	1992	DBLP DOI BibTeX RDF	membership proofs, languages, time complexity, polynomial time, independent set, clique, NP
23	Oded Goldreich 0001, Silvio Micali, Avi Wigderson	Proofs that Yield Nothing But Their Validity for All Languages in NP Have Zero-Knowledge Proof Systems.	J. ACM	1991	DBLP DOI BibTeX RDF	fault tolerant distributed computing, methodological design of protocols, cryptographic protocols, zero-knowledge, graph isomorphism, one-way functions, proof systems, NP, interactive proofs
23	Uriel Feige, Dror Lapidot, Adi Shamir	Multiple Non-Interactive Zero Knowledge Proofs Based on a Single Random String (Extended Abstract)	FOCS	1990	DBLP DOI BibTeX RDF	cryptographic applications, multiple noninteractive zero knowledge proofs, single random string, polynomially many provers, polynomially many theorems, open problems
23	Mihir Bellare, Oded Goldreich 0001, Shafi Goldwasser	Randomness in Interactive Proofs	FOCS	1990	DBLP DOI BibTeX RDF	coin tosses, error-reduction technique, Arthur-Merlin proof system, randomness, interactive proofs, sampling method
23	Anne Condon, Richard J. Lipton	On the Complexity of Space Bounded Interactive Proofs (Extended Abstract)	FOCS	1989	DBLP DOI BibTeX RDF	space bounded interactive proofs, finite-state verifiers, Markov chains, finite-state machines, upper bound, undecidable, interactive proof systems, recursively enumerable language
23	Joe Kilian, Silvio Micali, Rafail Ostrovsky	Minimum Resource Zero-Knowledge Proofs (Extended Abstract)	FOCS	1989	DBLP DOI BibTeX RDF	NP-theorems, oblivious transfer protocols, protocol, zero knowledge proofs, zero-knowledge protocols
23	Kevin D. Bowers, Ari Juels, Alina Oprea	HAIL: a high-availability and integrity layer for cloud storage.	CCS	2009	DBLP DOI BibTeX RDF	proofs of retrievability, erasure codes, data availability, distributed storage systems, cloud storage
23	Maria João Frade, Ando Saabas, Tarmo Uustalu	Bidirectional data-flow analyses, type-systematically.	PEPM	2009	DBLP DOI BibTeX RDF	mechanical transformation of program proofs, program analyses and optimizations, type systems, program logics
23	David Galindo	Breaking and Repairing Damgård et al. Public Key Encryption Scheme with Non-interactive Opening.	CT-RSA	2009	DBLP DOI BibTeX RDF	non-interactive proofs, standard model, public key encryption, identity-based encryption
23	John R. D. Hughes, Cliff B. Jones	Reasoning about programs via operational semantics: requirements for a support system.	Autom. Softw. Eng.	2008	DBLP DOI BibTeX RDF	Proofs about programs, Tool support, Structural operational semantics
23	Tatiana Yavorskaya	Interacting Explicit Evidence Systems.	Theory Comput. Syst.	2008	DBLP DOI BibTeX RDF	Justification logic, Explicit evidence, Logic of proofs, Epistemic logic, Multi-modal logic
23	Ali Bagherzandi, Jung Hee Cheon, Stanislaw Jarecki	Multisignatures secure under the discrete logarithm assumption and a generalized forking lemma.	CCS	2008	DBLP DOI BibTeX RDF	concurrent proofs of knowledge, equiocable homomorphic commitment, forking lemma, multisignatures
23	Shafi Goldwasser, Dan Gutfreund, Alexander Healy, Tali Kaufman, Guy N. Rothblum	Verifying and decoding in constant depth.	STOC	2007	DBLP DOI BibTeX RDF	error-correcting codes, interactive proofs, constant-depth circuits
23	Michael Beeson	Mathematical Induction in Otter-Lambda.	J. Autom. Reason.	2006	DBLP DOI BibTeX RDF	computer proofs, second-order, Otter, mathematical induction, unification, automated deduction
23	Orna Grumberg, Flavio Lerda, Ofer Strichman, Michael Theobald	Proof-guided underapproximation-widening for multi-process systems.	POPL	2005	DBLP DOI BibTeX RDF	SAT proofs, underapproximation-widening, abstraction, software verification, bounded model checking
23	Mircea-Dan Hernest	Light Functional Interpretation.	CSL	2005	DBLP DOI BibTeX RDF	Program extraction from (classical) proofs, Complexity of extracted programs, Berger’s uniform quantifiers, Functional interpretation, Proof Mining, Proof-Carrying Code
23	Abhik Roychoudhury, I. V. Ramakrishnan	Inductively Verifying Invariant Properties of Parameterized Systems.	Autom. Softw. Eng.	2004	DBLP DOI BibTeX RDF	induction proofs, logic programming, program transformations, concurrent systems, unfolding, folding, parameterized systems
23	Jeremy Avigad	Eliminating definitions and Skolem functions in first-order logic.	ACM Trans. Comput. Log.	2003	DBLP DOI BibTeX RDF	Skolem functions, lengths of proofs, Definitions, proof complexity
23	Ran Canetti, Hugo Krawczyk	Universally Composable Notions of Key Exchange and Secure Channels.	EUROCRYPT	2002	DBLP DOI BibTeX RDF	Composition of protocols, Cryptographic Protocols, Key Exchange, Proofs of Security
23	Oded Goldreich 0001	Concurrent zero-knowledge with timing, revisited.	STOC	2002	DBLP DOI BibTeX RDF	black-box simulation, proofs versus arguments, timing assumptions, zero-Knowledge, parallel composition, concurrent composition
23	Jacqueline Castaing	Non-commutative Logic for Hand-Written Character Modeling.	AISC	2002	DBLP DOI BibTeX RDF	Proofs Topics: Foundations and Complexity of Symbolic Computation, Logic and Symbolic Computing, Character Recognition, Linear Logic, Distance Computing
23	André Adelsbach, Ahmad-Reza Sadeghi	Zero-Knowledge Watermark Detection and Proof of Ownership.	Information Hiding	2001	DBLP DOI BibTeX RDF	Zero-Knowledge Watermark Detection, Ownership Proofs
23	Slawomir Lasota 0001	Behavioural Constructor Implementation for Regular Algebras.	LPAR	2000	DBLP DOI BibTeX RDF	regular algebras, behavioural constructor implementation, proofs of behavioural properties, Algebraic specifications, observational equivalence
23	Rostislav E. Yavorsky	On the Logic of the Standard Proof Predicate.	CSL	2000	DBLP DOI BibTeX RDF	logic of proofs, protocolling extensions of theories, semantics
23	Alessandro Armando, Alan Smaill, Ian Green	Automatic Synthesis of Recursive Programs: The Proof-Planning Paradigm.	ASE	1997	DBLP DOI BibTeX RDF	proof-planning paradigm, recursive functional programs, functional programming, correctness proofs, automatic synthesis, recursive programs, unification algorithm