Search results for "proof"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
18	James Brotherston, Alex Simpson	Complete Sequent Calculi for Induction and Infinite Descent.	LICS	2007	DBLP DOI BibTeX RDF
18	Dale Miller 0001, Vivek Nigam	Incorporating Tables into Proofs.	CSL	2007	DBLP DOI BibTeX RDF
18	Evelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons, Xavier Urbain	Certification of Automated Termination Proofs.	FroCoS	2007	DBLP DOI BibTeX RDF
18	Satrajit Chatterjee, Alan Mishchenko, Robert K. Brayton, Andreas Kuehlmann	On Resolution Proofs for Combinational Equivalence.	DAC	2007	DBLP DOI BibTeX RDF
18	Mridul Nandi	A Simple and Unified Method of Proving Indistinguishability.	INDOCRYPT	2006	DBLP DOI BibTeX RDF
18	Edward A. Hirsch, Sergey I. Nikolenko	Simulating Cutting Plane Proofs with Restricted Degree of Falsity by Resolution.	SAT	2005	DBLP DOI BibTeX RDF
18	Lars Engebretsen, Jonas Holmerin	More Efficient Queries in PCPs for NP and Improved Approximation Hardness of Maximum CSP.	STACS	2005	DBLP DOI BibTeX RDF
18	Guillaume Lussier, Hélène Waeselynck	Deriving Test Sets from Partial Proofs.	ISSRE	2004	DBLP DOI BibTeX RDF
18	Juan Carlos López Pimentel, Raúl Monroy	A Rippling-Based Difference Reduction Technique to Automatically Prove Security Protocol Goals.	IBERAMIA	2004	DBLP DOI BibTeX RDF
18	Sunae Seo, Hongseok Yang, Kwangkeun Yi	Automatic Construction of Hoare Proofs from Abstract Interpretation Results.	APLAS	2003	DBLP DOI BibTeX RDF
18	Eli Ben-Sasson, Avi Wigderson	Short proofs are narrow - resolution made simple.	J. ACM	2001	DBLP DOI BibTeX RDF
18	Joe Kilian, Erez Petrank	Concurrent and resettable zero-knowledge in poly-loalgorithm rounds.	STOC	2001	DBLP DOI BibTeX RDF
18	Colin Stirling	Schema Revisited.	CSL	2000	DBLP DOI BibTeX RDF
18	Ed Brinksma	Cache Consistency by Design.	Distributed Comput.	1999	DBLP DOI BibTeX RDF	Caching protocols, Correctness preserving, Transformations, Process algebra, Reactive systems, Formal design
18	Koichi Takahashi, Masami Hagiya	Proving as Editing HOL Tactics.	Formal Aspects Comput.	1999	DBLP DOI BibTeX RDF	Tactic-Based Theorem Prover, User interface, Higher Order Logic, Emacs
18	Serge Autexier, Dieter Hutter, Heiko Mantel, Axel Schairer	System Description: inka 5.0 - A Logic Voyager.	CADE	1999	DBLP DOI BibTeX RDF
18	Matthias Baaz, Alexander Leitsch, Georg Moser	System Description: CutRes 0.1: Cut Elimination by Resolution.	CADE	1999	DBLP DOI BibTeX RDF
18	Michael Balser, Wolfgang Reif, Gerhard Schellhorn, Kurt Stenzel	KIV 3.0 for Provably Correct Systems.	FM-Trends	1998	DBLP DOI BibTeX RDF
18	Peter Aczel	On Relating Type Theories and Set Theories.	TYPES	1998	DBLP DOI BibTeX RDF
18	Lassaad Cheikhrouhou, Jörg H. Siekmann	Planning Diagonalization Proofs.	AIMSA	1998	DBLP DOI BibTeX RDF
18	Peter V. Homeier, David F. Martin	Mechanical Verification of Mutually Recursive Procedures.	CADE	1996	DBLP DOI BibTeX RDF
18	Satyanarayana V. Lokam, Meena Mahajan, V. Vinay	Logspace Verifiers, NC, and NP.	ISAAC	1995	DBLP DOI BibTeX RDF
18	Huimin Lin	Complete Inference Systems for Weak Bisimulation Equivalences in the pi-Calculus.	TAPSOFT	1995	DBLP DOI BibTeX RDF
18	Lidong Chen, Ivan Damgård, Torben P. Pedersen	Parallel Divertibility of Proofs of Knowledge (Extended Abstract).	EUROCRYPT	1994	DBLP DOI BibTeX RDF
18	Jane Hesketh, Alan Bundy, Alan Smaill	Using Middle-Out Reasoning to Control the Synthesis of Tail-Recursive Programs.	CADE	1992	DBLP DOI BibTeX RDF
18	A. Puccetti	The Integrated Software Development and Verification System ATES.	VDM Europe (1)	1991	DBLP DOI BibTeX RDF
18	Amy P. Felty	A Logic Program for Transforming Sequent Proofs to Natural Deduction Proofs.	ELP	1989	DBLP DOI BibTeX RDF
18	Martin Davis, Hilary Putnam	A Computing Procedure for Quantification Theory.	J. ACM	1960	DBLP DOI BibTeX RDF
18	Jasmin Christian Blanchette	Proof Pearl: Mechanizing the Textbook Proof of Huffman's Algorithm.	J. Autom. Reason.	2009	DBLP DOI BibTeX RDF	Interactive theorem provers, Huffman coding, Higher-order logic
18	Wuming Pan, Bing Guo	Nested Proof Compilation and Proof Checking in Universal Pattern Logic.	RSKT	2009	DBLP DOI BibTeX RDF
18	Sylvie Boldo	Pitfalls of a Full Floating-Point Proof: Example on the Formal Proof of the Veltkamp/Dekker Algorithms.	IJCAR	2006	DBLP DOI BibTeX RDF
18	Deepak Garg 0001, Frank Pfenning	A Proof-Carrying File System.	IEEE Symposium on Security and Privacy	2010	DBLP DOI BibTeX RDF	proof-carrying authorization, Access control, logic, file system
18	Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli	User Interaction with the Matita Proof Assistant.	J. Autom. Reason.	2007	DBLP DOI BibTeX RDF	Mathematical knowledge management, XML, Digital libraries, Authoring, Interactive theorem proving, Proof assistant
18	Patrick Blackburn, Balder ten Cate	Pure Extensions, Proof Rules, and Hybrid Axiomatics.	Stud Logica	2006	DBLP DOI BibTeX RDF	completeness, modal logic, Hybrid logic, proof rules, axiomatisation, nominals
18	Matthew Stone	Disjunction and modular goal-directed proof search.	ACM Trans. Comput. Log.	2005	DBLP DOI BibTeX RDF	goal-directed proof, indefinite information, locality, logic programming, modularity, Modal logic
18	Dominic J. D. Hughes, Rob J. van Glabbeek	Proof nets for unit-free multiplicative-additive linear logic.	ACM Trans. Comput. Log.	2005	DBLP DOI BibTeX RDF	Linear logic, cut elimination, additives, proof nets
18	Amos Korman, Shay Kutten, David Peleg	Proof labeling schemes.	PODC	2005	DBLP DOI BibTeX RDF	proof labels, self stabilization, distributed networks, property verification
18	Takayuki Suyama, Makoto Yokoo	Strategy/false-name proof protocols for combinatorial multi-attribute procurement auction: handling arbitrary utility of the buyer.	AAMAS	2005	DBLP DOI BibTeX RDF	false-name-proof, combinatorial auction, multi-attribute
18	Aarne Ranta, Robin Cooper	Dialogue Systems as Proof Editors.	J. Log. Lang. Inf.	2004	DBLP DOI BibTeX RDF	proof editing, type theory, dialogue
18	Chris GauthierDickey, Daniel Zappala, Virginia Mary Lo, James Marr	Low latency and cheat-proof event ordering for peer-to-peer games.	NOSSDAV	2004	DBLP DOI BibTeX RDF	cheat-proof, peer-to-peer, interactive, games, distributed, low-latency
18	Raúl Monroy	Predicate Synthesis for Correcting Faulty Conjectures: The Proof Planning Paradigm.	Autom. Softw. Eng.	2003	DBLP DOI BibTeX RDF	faulty specifications, program synthesis/transformation, abduction, proof planning
18	Martin Fränzle, Christian Herde	Efficient SAT Engines for Concise Logics: Accelerating Proof Search for Zero-One Linear Constraint Systems.	LPAR	2003	DBLP DOI BibTeX RDF	non-clausal propositional logic, zero-one linear constraint systems, Satisfiability, proof search, acceleration techniques
18	Andrei Voronkov	How to optimize proof-search in modal logics: new methods of proving redundancy criteria for sequent calculi.	ACM Trans. Comput. Log.	2001	DBLP DOI BibTeX RDF	theorem proving, modal logic, description logics, proof-search, inverse method
18	Bev Littlewood	The Use of Proof in Diversity Arguments.	IEEE Trans. Software Eng.	2000	DBLP DOI BibTeX RDF	reliability, verification, probability, safety, Software fault tolerance, proof
18	Michael Alekhnovich, Eli Ben-Sasson, Alexander A. Razborov, Avi Wigderson	Pseudorandom Generators in Propositional Proof Complexity.	FOCS	2000	DBLP DOI BibTeX RDF	combinatorial pseudorandom generators, Nisan-Wigderson generator, Tseitin tautologies, polynomial calculus with resolution, polynomial calculus, computational complexity, theorem proving, process algebra, resolution, random processes, pseudorandom generators, propositional proof complexity
18	Claudia Faggian	Proof construction and non-commutativity: a cluster calculus.	PPDP	2000	DBLP DOI BibTeX RDF	non-commutative logic, logic programming, linear logic, proof search, focalization
18	Sanjeev Arora, Carsten Lund, Rajeev Motwani 0001, Madhu Sudan 0001, Mario Szegedy	Proof Verification and Hardness of Approximation Problems	FOCS	1992	DBLP DOI BibTeX RDF	approximation problems, polynomial-time probabilistic oracle machine, random bits, MAXSNP-hard, metric TSP, time complexity, NP, MAX-CUT, MAX-SAT, proof verification
18	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
18	Carsten Lund, Lance Fortnow, Howard J. Karloff, Noam Nisan	Algebraic Methods for Interactive Proof Systems	FOCS	1990	DBLP DOI BibTeX RDF	polynomial value verification, program self correction, algebraic technique, program verification, language, interactive proof systems, program checking, polynomial-time hierarchy, low-degree polynomial
18	Ahmed K. Elmagarmid, Neelam Soundararajan, Ming T. Liu	A Distributed Deadlock Detection and Resolution Algorithm and Its Correctness Proof.	IEEE Trans. Software Eng.	1988	DBLP DOI BibTeX RDF	transaction controller, distributed processing, program verification, transaction processing, transaction processing, programming theory, system recovery, communicating sequential processes, correctness proof, distributed deadlock detection
18	Deepak Kapur, Paliath Narendran, Hantao Zhang 0001	Proof by Induction Using Test Sets.	CADE	1986	DBLP DOI BibTeX RDF	Inductionless Induction, Knuth-Bendix Completion Procedure, Consistency, Induction, Equational Theory, Sufficient-Completeness, Proof by Induction
18	Ralph L. London	Certification of algorithm 245 [M1]: treesort 3: proof of algorithms - a new kind of certification.	Commun. ACM	1970	DBLP DOI BibTeX RDF	in-place sorting, metatheory, proof of algorithms, debugging, sorting, certification
17	Martin C. Rinard	Integrated Reasoning and Proof Choice Point Selection in the Jahob System - Mechanisms for Program Survival.	CADE	2009	DBLP DOI BibTeX RDF
17	Luís Pinto 0001, Tarmo Uustalu	Proof Search and Counter-Model Construction for Bi-intuitionistic Propositional Logic with Labelled Sequents.	TABLEAUX	2009	DBLP DOI BibTeX RDF
17	Michelle Graham, David Gray	Protecting Privacy and Securing the Gathering of Location Proofs - The Secure Location Verification Proof Gathering Protocol.	MobiSec	2009	DBLP DOI BibTeX RDF
17	Morten Kühnrich, Uwe Nestmann	On Process-Algebraic Proof Methods for Fault Tolerant Distributed Systems.	FMOODS/FORTE	2009	DBLP DOI BibTeX RDF
17	Grigore Rosu, Dorel Lucanu	Circular Coinduction: A Proof Theoretical Foundation.	CALCO	2009	DBLP DOI BibTeX RDF
17	Richard Cleve, William Slofstra, Falk Unger, Sarvagya Upadhyay	Perfect Parallel Repetition Theorem for Quantum Xor Proof Systems.	Comput. Complex.	2008	DBLP DOI BibTeX RDF	Subject classification. 81P68, 68Q10
17	Erik Meijer 0002, Jelmer Y. Ypma	A Simple Identification Proof for a Mixture of Two Univariate Normal Distributions.	J. Classif.	2008	DBLP DOI BibTeX RDF	Information matrix, Mixture regression, Finite mixtures, Exponential family
17	Jesús Aransay, Clemens Ballarin, Julio Rubio 0001	A Mechanized Proof of the Basic Perturbation Lemma.	J. Autom. Reason.	2008	DBLP DOI BibTeX RDF	Homological algebra, Basic perturbation lemma, Isabelle
17	H. Jaap van den Herik, Mark H. M. Winands	Proof-Number Search and Its Variants.	Oppositional Concepts in Computational Intelligence	2008	DBLP DOI BibTeX RDF
17	James Worthington	Automatic Proof Generation in Kleene Algebra.	RelMiCS	2008	DBLP DOI BibTeX RDF
17	Florin Craciun, Shengchao Qin, Wei-Ngan Chin	A Formal Soundness Proof of Region-Based Memory Management for Object-Oriented Paradigm.	ICFEM	2008	DBLP DOI BibTeX RDF
17	Grigori Mints	Proof Search Tree and Cut Elimination.	Pillars of Computer Science	2008	DBLP DOI BibTeX RDF
17	Eelis van der Weegen, James McKinna	A Machine-Checked Proof of the Average-Case Complexity of Quicksort in Coq.	TYPES	2008	DBLP DOI BibTeX RDF
17	Cezary Kaliszyk, Freek Wiedijk	Merging Procedural and Declarative Proof.	TYPES	2008	DBLP DOI BibTeX RDF
17	Ugo Dal Lago, Martin Hofmann 0001	A Semantic Proof of Polytime Soundness of Light Affine Logic.	CSR	2008	DBLP DOI BibTeX RDF
17	Pavel Pudlák	Twelve Problems in Proof Complexity.	CSR	2008	DBLP DOI BibTeX RDF
17	John Derrick, Gerhard Schellhorn, Heike Wehrheim	Mechanizing a Correctness Proof for a Lock-Free Concurrent Stack.	FMOODS	2008	DBLP DOI BibTeX RDF	non-atomic refinement, KIV, refinement, theorem proving, Z, linearizability, concurrent access
17	Jacques Patarin	A Proof of Security in O(2n) for the Benes Scheme.	AFRICACRYPT	2008	DBLP DOI BibTeX RDF	information-theoretic primitive, design of keyed hash functions, security above the birthday bound, unconditional security, Pseudorandom function
17	Dominik Dietrich, Ewaryst Schulz, Marc Wagner 0001	Authoring Verified Documents by Interactive Proof Construction and Verification in Text-Editors.	AISC/MKM/Calculemus	2008	DBLP DOI BibTeX RDF
17	Marc Fuentes	Diagonalization of the symmetrized discrete i th right shift operator: an elementary proof.	Numer. Algorithms	2007	DBLP DOI BibTeX RDF	Discrete right shift operator, Eigenvalues, Eigenvectors
17	Pierluigi Minari	Analytic proof systems for lambda-calculus: the elimination of transitivity, and why it matters.	Arch. Math. Log.	2007	DBLP DOI BibTeX RDF	Mathematics Subject Classification (2000) 03B40, 03F03, 03F07, 03F05
17	Minos N. Garofalakis, Joseph M. Hellerstein, Petros Maniatis	Proof Sketches: Verifiable In-Network Aggregation.	ICDE	2007	DBLP DOI BibTeX RDF
17	Thomas Vetterlein	Towards a Proof Theory for Basic Logic.	IFSA (2)	2007	DBLP DOI BibTeX RDF
17	Pierre Corbineau	A Declarative Language for the Coq Proof Assistant.	TYPES	2007	DBLP DOI BibTeX RDF
17	A. R. Dani, Arun K. Pujari, Ved Prakash Gulati	Strategy proof electronic markets.	ICEC	2007	DBLP DOI BibTeX RDF	demand reduction, multi agent systems, mechanism design, electronic markets, double auction
17	Toni Jussila, Armin Biere, Carsten Sinz, Daniel Kröning, Christoph M. Wintersteiger	A First Step Towards a Unified Proof Checker for QBF.	SAT	2007	DBLP DOI BibTeX RDF
17	Virgile Mogbil, Vincent Rahli	Uniform Circuits, & Boolean Proof Nets.	LFCS	2007	DBLP DOI BibTeX RDF
17	Paulin Jacobé de Naurois, Virgile Mogbil	Correctness of Multiplicative (and Exponential) Proof Structures is NL -Complete.	CSL	2007	DBLP DOI BibTeX RDF
17	Richard Cleve, William Slofstra, Falk Unger, Sarvagya Upadhyay	Perfect Parallel Repetition Theorem for Quantum XOR Proof Systems.	CCC	2007	DBLP DOI BibTeX RDF
17	Jeremy Avigad	Mathematical Method and Proof.	Synth.	2006	DBLP DOI BibTeX RDF
17	Solange Coupet-Grimal, William Delobel	An effective proof of the well-foundedness of the multiset path ordering.	Appl. Algebra Eng. Commun. Comput.	2006	DBLP DOI BibTeX RDF	Well-foundedness, Multiset path order, Termination, Constructive logic
17	Richard Bonichon, Olivier Hermant	A Semantic Completeness Proof for TaMeD.	LPAR	2006	DBLP DOI BibTeX RDF
17	Kazuhiro Ogata 0001, Kokichi Futatsugi	Some Tips on Writing Proof Scores in the OTS/CafeOBJ Method.	Essays Dedicated to Joseph A. Goguen	2006	DBLP DOI BibTeX RDF
17	Sebastian Golze, Gero Mühl	Fair Overload Handling Using Proof-of-Work Functions.	SAINT	2006	DBLP DOI BibTeX RDF
17	Grigori Mints	Unwinding a Non-effective Cut Elimination Proof.	CSR	2006	DBLP DOI BibTeX RDF
17	Joachim Biskup, Lena Wiese	On Finding an Inference-Proof Complete Database for Controlled Query Evaluation. (PDF / PS)	DBSec	2006	DBLP DOI BibTeX RDF	confidentiality of data, complete database systems, Branch and Bound, propositional logic, inference control, SAT solving, lying, Controlled Query Evaluation
17	Stephanie Wehner	Entanglement in Interactive Proof Systems with Binary Answers.	STACS	2006	DBLP DOI BibTeX RDF
17	Pascal Fontaine, Jean-Yves Marion, Stephan Merz, Leonor Prensa Nieto, Alwen Fernanto Tiu	Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants.	TACAS	2006	DBLP DOI BibTeX RDF
17	Florent Bouchez, Alain Darte, Christophe Guillon, Fabrice Rastello	Register Allocation: What Does the NP-Completeness Proof of Chaitin et al. Really Prove? Or Revisiting Register Allocation: Why and How.	LCPC	2006	DBLP DOI BibTeX RDF
17	Jan Krajícek	Forcing with Random Variables and Proof Complexity.	CiE	2006	DBLP DOI BibTeX RDF
17	Pim Tuyls, Geert Jan Schrijen, Boris Skoric, Jan van Geloven, Nynke Verhaegh, Rob Wolters	Read-Proof Hardware from Protective Coatings.	CHES	2006	DBLP DOI BibTeX RDF
17	Heiko Mantel, Henning Sudbrock, Tina Kraußer	Combining Different Proof Techniques for Verifying Information Flow Security.	LOPSTR	2006	DBLP DOI BibTeX RDF
17	Matthias Baaz, Stefan Hetzl, Alexander Leitsch, Clemens Richter, Hendrik Spohr	Proof Transformation by CERES.	MKM	2006	DBLP DOI BibTeX RDF
17	Clemens Ballarin	Interpretation of Locales in Isabelle: Theories and Proof Contexts.	MKM	2006	DBLP DOI BibTeX RDF
17	Amy P. Felty	A Tutorial Example of the Semantic Approach to Foundational Proof-Carrying Code: Abstract.	TLCA	2005	DBLP DOI BibTeX RDF
17	Kim-Kwang Raymond Choo, Colin Boyd, Yvonne Hitchcock	Examining Indistinguishability-Based Proof Models for Key Establishment Protocols.	ASIACRYPT	2005	DBLP DOI BibTeX RDF
17	Serge Autexier	On the Dynamic Increase of Multiplicities in Matrix Proof Methods for Classical Higher-Order Logic.	TABLEAUX	2005	DBLP DOI BibTeX RDF
17	Amy P. Felty	A Tutorial Example of the Semantic Approach to Foundational Proof-Carrying Code.	RTA	2005	DBLP DOI BibTeX RDF