Search results for "proof"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
27	Philip W. L. Fong, Robert D. Cameron	Proof linking: modular verification of mobile programs in the presence of lazy, dynamic linking.	ACM Trans. Softw. Eng. Methodol.	2000	DBLP DOI BibTeX RDF	correctness conditions, proof linking, verification protocol, virtual machine architecture, Java, modularity, safety, mobile code, dynamic linking
27	Luc Bougé, David Cachera	On the Completeness of a Proof System for a Simple Data-Parallel Programming Language.	Euro-Par	1995	DBLP DOI BibTeX RDF	Specifying and Verifying and Reasoning about Programs, Concurrent Programming, Hoare Logic, Weakest Preconditions, Proof System, Data-Parallel Languages, Semantics of Programming Languages
27	Marco Alberti 0001, Federico Chesani, Marco Gavanelli, Evelina Lamma, Paola Mello, Paolo Torroni	Verifiable agent interaction in abductive logic programming: The SCIFF framework.	ACM Trans. Comput. Log.	2008	DBLP DOI BibTeX RDF	Abductive logic programming, IFF proof procedure, SCIFF, SOCS (SOcieties of ComputeeS), formal properties, proof-procedures, declarative semantics, agent interaction protocols
27	Mark Nicholas Charles Rhodes	Rank Lower Bounds for the Sherali-Adams Operator.	CiE	2007	DBLP DOI BibTeX RDF	Lift and Project Proof Systems, Rank Lower Bounds, Sherali-Adams Relaxation, Propositional Proof Complexity
27	Carlos Simpson	Explaining Gabriel-Zisman Localization to the Computer.	J. Autom. Reason.	2006	DBLP DOI BibTeX RDF	calculus of fractions, computer proof verification, localization, category, proof assistant, functor
27	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
27	Joseph A. Goguen, Kai Lin, Akira Mori, Grigore Rosu, Akiyoshi Sato	Distributed Cooperative Formal Methods Tools.	ASE	1997	DBLP DOI BibTeX RDF	distributed cooperative formal methods tools, distributed cooperative proving, proof editor, remote proof execution, distributed truth protocol, editor generator, algebraic semiotics, interface design, algebraic specification, algebraic specification
27	Zuoquan Lin, Wei Li 0022	On Logic of Paradox.	ISMVL	1995	DBLP DOI BibTeX RDF	logic of paradox, minimal semantics, satisfactory proof theory, signed tableaux, completeness theorems, theorem proving, soundness, nonmonotonic reasoning, proof theory, paraconsistent logic, nonmonotonicity
26	Lawrence C. Paulson, Kong Woei Susanto	Source-Level Proof Reconstruction for Interactive Theorem Proving.	TPHOLs	2007	DBLP DOI BibTeX RDF
26	Judi Romijn, Wieger Wesselink, Arjan J. Mooij	Assertion-Based Proof Checking of Chang-Roberts Leader Election in PVS.	ATVA	2007	DBLP DOI BibTeX RDF
26	Olaf Beyersdorff	Disjoint NP-Pairs from Propositional Proof Systems.	TAMC	2006	DBLP DOI BibTeX RDF
26	Yoram Moses, Benny Shimony	A New Proof of the GHS Minimum Spanning Tree Algorithm.	DISC	2006	DBLP DOI BibTeX RDF
26	Milos Besta, Frank A. Stomp	An Assertional Correctness Proof of a Self-Stabilizing - Exclusion Algorithm.	ICECCS	2006	DBLP DOI BibTeX RDF
26	Armin Fiedler	Natural Language Proof Explanation.	Mechanizing Mathematical Reasoning	2005	DBLP DOI BibTeX RDF
26	Alan Bundy	Planning and Patching Proof.	AISC	2004	DBLP DOI BibTeX RDF
26	Gunnar Andersson, Per Bjesse, Byron Cook, Ziyad Hanna	Design automation with mixtures of proof strategies for propositional logic.	IEEE Trans. Comput. Aided Des. Integr. Circuits Syst.	2003	DBLP DOI BibTeX RDF
26	Hans-Gert Gräbe	The SymbolicData GEO Records - A Public Repository of Geometry Theorem Proof Schemes.	Automated Deduction in Geometry	2002	DBLP DOI BibTeX RDF
26	Jochen Messner	On the Structure of the Simulation Order of Proof Systems.	MFCS	2002	DBLP DOI BibTeX RDF
26	Matthias Baaz	Proof Analysis by Resolution.	CADE	2002	DBLP DOI BibTeX RDF
26	Alfredo De Santis, Giovanni Di Crescenzo, Giuseppe Persiano	Randomness-Optimal Characterization of Two NP Proof Systems.	RANDOM	2002	DBLP DOI BibTeX RDF
26	Jacques Stern, David Pointcheval, John Malone-Lee, Nigel P. Smart	Flaws in Applying Proof Methodologies to Signature Schemes.	CRYPTO	2002	DBLP DOI BibTeX RDF
26	Raúl Monroy	Concept Formation via Proof Planning Failure.	LPAR	2001	DBLP DOI BibTeX RDF
26	Stephan Schmitt, Lori Lorigo, Christoph Kreitz, Aleksey Nogin	JProver : Integrating Connection-Based Theorem Proving into Interactive Proof Assistants.	IJCAR	2001	DBLP DOI BibTeX RDF
26	Miyuki Koshimura, Ryuzo Hasegawa	Proof Simplification for Model Generation and Its Applications.	LPAR	2000	DBLP DOI BibTeX RDF
26	Thomas Hallgren, Aarne Ranta	An Extensible Proof Text Editor.	LPAR	2000	DBLP DOI BibTeX RDF
26	Gilles Dowek	Proof Normalization for a First-Order Formulation of Higher-Order Logic.	TPHOLs	1997	DBLP DOI BibTeX RDF
26	Klaus Schneider 0001, Ramayya Kumar, Thomas Kropf	Alternative Proof Procedures for Finite-State Machines in Higher-Order Logic.	HUG	1993	DBLP DOI BibTeX RDF
26	Knut Hinkelmann, Helge Hintze	Computing Cost Estimates for Proof Strategies.	ELP	1993	DBLP DOI BibTeX RDF
26	Bishop Brock, Shaun Cooper, William Pierce	Analogical Reasoning and Proof Discovery.	CADE	1988	DBLP DOI BibTeX RDF
25	Adam Chlipala	A verified compiler for an impure functional language.	POPL	2010	DBLP DOI BibTeX RDF	compiler verification, interactive proof assistants
25	Oded Fuhrmann, Shlomo Hoory	On Extending Bounded Proofs to Inductive Proofs.	CAV	2009	DBLP DOI BibTeX RDF	resolution proofs, extending proofs, proof simplification, Formal verification
25	Gilles Barthe, Benjamin Grégoire, Santiago Zanella Béguelin	Formal certification of code-based cryptographic proofs.	POPL	2009	DBLP DOI BibTeX RDF	cryptographic proofs, relational hoare logic, program transformations, observational equivalence, coq proof assistant
25	Adam Chlipala, J. Gregory Malecha, Greg Morrisett, Avraham Shinnar, Ryan Wisnesky	Effective interactive proofs for higher-order imperative programs.	ICFP	2009	DBLP DOI BibTeX RDF	functional programming, dependent types, separation logic, interactive proof assistants
25	Ugo Dal Lago, Luca Roversi, Luca Vercelli	Taming Modal Impredicativity: Superlazy Reduction.	LFCS	2009	DBLP DOI BibTeX RDF	Linear logic, proof theory, implicit computational complexity
25	Olaf Beyersdorff	Tuples of Disjoint NP-Sets.	Theory Comput. Syst.	2008	DBLP DOI BibTeX RDF	Propositional proof systems, Disjoint -pairs
25	James Brotherston, Richard Bornat, Cristiano Calcagno	Cyclic proofs of program termination in separation logic.	POPL	2008	DBLP DOI BibTeX RDF	cyclic proof, program verification, termination, hoare logic, separation logic, inductive definitions
25	Jakob Nordström, Johan Håstad	Towards an optimal separation of space and length in resolution.	STOC	2008	DBLP DOI BibTeX RDF	length, lower bound, resolution, space, separation, pebbling, proof complexity
25	David Nowak	A Framework for Game-Based Security Proofs.	ICICS	2007	DBLP DOI BibTeX RDF	security, game, formal verification, proof assistant
25	Zhengjun Cao, Lihua Liu	Boudot's Range-Bounded Commitment Scheme Revisited.	ICICS	2007	DBLP DOI BibTeX RDF	range-bounded commitment, knowledge of a discrete logarithm, zero-knowledge proof
25	Ravi Kumar 0001, D. Sivakumar 0001	Proofs, Codes, and Polynomial-Time Reducibilities.	CCC	1999	DBLP DOI BibTeX RDF	reducibilities, proof systems, partial solutions
25	Maria Luisa Bonet, Toniann Pitassi, Ran Raz	No Feasible Interpolation for TC0-Frege Proofs.	FOCS	1997	DBLP DOI BibTeX RDF	TC/sup 0/-Frege proofs, feasible interpolation, complexity-theoretic assumption, hardness assumption, lower bounds, theorem proving, Chinese Remainder Theorem, proof systems
24	Omer Reingold, Luca Trevisan, Madhur Tulsiani, Salil P. Vadhan	Dense Subsets of Pseudorandom Sets.	FOCS	2008	DBLP DOI BibTeX RDF
24	David Baelde, Dale Miller 0001	Least and Greatest Fixed Points in Linear Logic.	LPAR	2007	DBLP DOI BibTeX RDF
24	Adam J. Lee, Kazuhiro Minami, Marianne Winslett	Lightweight cnsistency enforcement schemes for distributed proofs with hidden subtrees.	SACMAT	2007	DBLP DOI BibTeX RDF	distributed proving, pervasive computing, consistency
24	James Brotherston	Formalised Inductive Reasoning in the Logic of Bunched Implications.	SAS	2007	DBLP DOI BibTeX RDF
24	Erica Melis, Martin Pollet, Jörg H. Siekmann	Reductio ad Absurdum: Planning Proofs by Contradiction.	Reasoning, Action and Interaction in AI Theories and Systems	2006	DBLP DOI BibTeX RDF
24	Eli Ben-Sasson, Oded Goldreich 0001, Prahladh Harsha, Madhu Sudan 0001, Salil P. Vadhan	Short PCPs Verifiable in Polylogarithmic Time.	CCC	2005	DBLP DOI BibTeX RDF
24	Grigore Rosu, Steven Eker, Patrick Lincoln, José Meseguer 0001	Certifying and Synthesizing Membership Equational Proofs.	FME	2003	DBLP DOI BibTeX RDF
24	John Watrous	imits on the Power of Quantum Statistical Zero-Knowledge.	FOCS	2002	DBLP DOI BibTeX RDF
24	Mateja Jamnik, Manfred Kerber, Martin Pollet	Learn Omega-matic: System Description.	CADE	2002	DBLP DOI BibTeX RDF
24	James O. Henriksen	Adding animation to a simulation using ProofTM.	WSC	2000	DBLP DOI BibTeX RDF
24	Leendert W. N. van der Torre	Phased Labeled Logics of Conditional Goals.	JELIA	1998	DBLP DOI BibTeX RDF
24	Giovanni Di Crescenzo, Tatsuaki Okamoto, Moti Yung	Keeping the SZK-Verifier Honest Unconditionally.	CRYPTO	1997	DBLP DOI BibTeX RDF
24	Francisco-Jesús Martín-Mateos, José-Luis Ruiz-Reina, José-Antonio Alonso, María-José Hidalgo	Proof Pearl: A Formal Proof of Higman's Lemma in ACL2.	TPHOLs	2005	DBLP DOI BibTeX RDF
24	George C. Necula, Robert R. Schneck	Proof-Carrying Code with Untrusted Proof Rules.	ISSS	2002	DBLP DOI BibTeX RDF
24	Olivier Laurent 0001	Polarized Proof-Nets: Proof-Nets for LC.	TLCA	1999	DBLP DOI BibTeX RDF
24	Chin-Liang Chang	The Unit Proof and the Input Proof in Theorem Proving.	J. ACM	1970	DBLP DOI BibTeX RDF
24	Brittany A. Duncan, Robin R. Murphy, Dylan A. Shell, Amy G. Hopper	A midsummer night's dream: social proof in HRI.	HRI	2010	DBLP DOI BibTeX RDF	robotic theater, social proof, uav-human interaction, human-robot interaction, social interaction, performing arts
24	Dominique Cansell, Dominique Méry, Cyril Proch	System-on-chip design by proof-based refinement.	Int. J. Softw. Tools Technol. Transf.	2009	DBLP DOI BibTeX RDF	Event B method, Simulation, System-on-chip, Refinement, Formal modelling, Operational semantics, SystemC, Proof
24	Yuichi Komano, Kazuo Ohta, Hideyuki Miyake, Atsushi Shimbo	Algorithmic Tamper Proof (ATP) Counter Units for Authentication Devices Using PIN.	ACNS	2009	DBLP DOI BibTeX RDF	algorithmic tamper proof (ATP), counter unit, PIN authentication
24	Thomas Studer	On the Proof Theory of the Modal mu-Calculus.	Stud Logica	2008	DBLP DOI BibTeX RDF	Infinitary proof theory, ?-calculus
24	Hasan Amjad	Data Compression for Proof Replay.	J. Autom. Reason.	2008	DBLP DOI BibTeX RDF	Proof translation, Interactive theorem proving, SAT solvers
24	Paulo F. Silva 0001, José Nuno Oliveira	'Galculator': functional prototype of a Galois-connection based proof assistant.	PPDP	2008	DBLP DOI BibTeX RDF	point-free notation, haskell, DSL, Galois connections, proof assistant, GADT
24	Chunxiao Lin, Yiyun Chen, Long Li, Bei Hua	Garbage Collector Verification for Proof-Carrying Code.	J. Comput. Sci. Technol.	2007	DBLP DOI BibTeX RDF	program safety, program verification, proof-carrying code, garbage collector
24	Sergej Sizov	What Makes You Think That? The Semantic Web's Proof Layer.	IEEE Intell. Syst.	2007	DBLP DOI BibTeX RDF	proof layer, provenance knowledge, self-organizing knowledge, automated agents, Semantic Web, Web browsing
24	Katie Atkinson, Trevor J. M. Bench-Capon	Argumentation and standards of proof.	ICAIL	2007	DBLP DOI BibTeX RDF	standards of proof, argumentation, legal reasoning, purposes
24	Guillaume Burel	Unbounded Proof-Length Speed-Up in Deduction Modulo.	CSL	2007	DBLP DOI BibTeX RDF	rewriting, arithmetic, higher order logic, proof theory
24	Xavier Leroy	Formal certification of a compiler back-end or: programming a compiler with a proof assistant.	POPL	2006	DBLP DOI BibTeX RDF	compiler transformations and optimizations, the Coq theorem prover, certified compilation, program proof, semantic preservation
24	Makoto Yokoo, Toshihiro Matsutani, Atsushi Iwasaki	False-name-proof combinatorial auction protocol: Groves Mechanism with SubModular Approximation.	AAMAS	2006	DBLP DOI BibTeX RDF	strategy-proof, combinatorial auction
24	Morten P. Lindegaard, Anne E. Haxthausen	Proof Support for RAISE by a Reuse Approach Based on Institutions.	AMAST	2004	DBLP DOI BibTeX RDF	proof support, Institutions, algebraic semantics, HOL, RSL
24	Harumichi Nishimura, Tomoyuki Yamakami	An Application of Quantum Finite Automata to Interactive Proof Systems.	CIAA	2004	DBLP DOI BibTeX RDF	quantum finite automaton, quantum interactive proof system, quantum measurement, quantum circuit
24	Dale Miller 0001, Alwen Fernanto Tiu	A Proof Theory for Generic Judgments: An extended abstract.	LICS	2003	DBLP DOI BibTeX RDF	reasoning about operational semantics, generic judgments, higher-order abstract syntax, proof search
24	Ichiro Ogata	A Proof Theoretical Account of Continuation Passing Style.	CSL	2002	DBLP DOI BibTeX RDF	Classical Natural Deduction, LKQ, classical proof theory, Classical Logic, CPS-translation, Call-By-Value
24	Carlos H. C. Duarte	Towards a Proof-Theoretic Foundation for Actor Specification and Verification.	ModelAge Workshop	1997	DBLP DOI BibTeX RDF	Distributed Systems, Verification, Specification, Actors, Proof-Theory
24	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
24	Leo Bachmair, Nachum Dershowitz	Equational Inference, Canonical Proofs, and Proof Orderings.	J. ACM	1994	DBLP DOI BibTeX RDF	term rewriting, rewrite systems, proof theory, equational logic, inference systems, term orderings
24	Carsten Lund, Lance Fortnow, Howard J. Karloff, Noam Nisan	Algebraic Methods for Interactive Proof Systems.	J. ACM	1992	DBLP DOI BibTeX RDF	interactive proof systems
24	Fred B. Schneider, Bard Bloom, Keith Marzullo	Putting Time into Proof Outlines.	REX Workshop	1991	DBLP DOI BibTeX RDF	concurrent program verification, real-time actions, proof outlines, safety properties, real-time programming, timing properties
23	Konstantine Arkoudas	Simplifying Proofs in Fitch-Style Natural Deduction Systems.	J. Autom. Reason.	2005	DBLP DOI BibTeX RDF	Fitch style, proof simplification, denotational proof languages, NDL, assumption bases, natural deduction, detours
23	Jean-Raymond Abrial, Dominique Cansell, Dominique Méry	A Mechanically Proved and Incremental Development of IEEE 1394 Tree Identify Protocol.	Formal Aspects Comput.	2003	DBLP DOI BibTeX RDF	Proof-based development, Proof engine, Refinement, B method, Abstract model, Event-driven approach
23	Stephen Paynter, James M. Armstrong, Jan Haveman	ADL: An Activity Description Language for Real-Time Networks.	Formal Aspects Comput.	2000	DBLP DOI BibTeX RDF	Proof-theoretic semantics, Proof of timeliness, Formal specifications, ADL, Real-time processes
23	Shafi Goldwasser	New Directions in Cryptography: Twenty Some Years Later.	FOCS	1997	DBLP DOI BibTeX RDF	probabilistic proof systems, cryptography, cryptography, complexity theory, interactive proof systems, pseudo random number generation
23	David A. McAllester, Robert Givan	Taxonomic Syntax for First Order Inference.	J. ACM	1993	DBLP DOI BibTeX RDF	machine inference, theorem proving, polynomial time algorithms, automated reasoning, inference rules, proof theory, proof systems, mechanical verification
23	Lutz Straßburger	Some Observations on the Proof Theory of Second Order Propositional Multiplicative Linear Logic.	TLCA	2009	DBLP DOI BibTeX RDF
23	Clément Hurlin	Automatic Parallelization and Optimization of Programs by Proof Rewriting.	SAS	2009	DBLP DOI BibTeX RDF
23	Stefan Hetzl, Alexander Leitsch, Daniel Weller 0001, Bruno Woltzenlogel Paleo	A Clausal Approach to Proof Analysis in Second-Order Logic.	LFCS	2009	DBLP DOI BibTeX RDF
23	Salah Merniz, Mohamed Benmohammed	A Scalable Proof Methodology for RISC Processor Designs: A Functional Approach.	ITNG	2008	DBLP DOI BibTeX RDF	State functions, RISC designs, Formal Verification, Functional programming, Micro-architectures
23	Michal Moskal	Rocket-Fast Proof Checking for SMT Solvers.	TACAS	2008	DBLP DOI BibTeX RDF
23	René David, Karim Nour	An Arithmetical Proof of the Strong Normalization for the lambda -Calculus with Recursive Equations on Types.	TLCA	2007	DBLP DOI BibTeX RDF
23	Roman Kuznets	Proof Identity for Classical Logic: Generalizing to Normality.	LFCS	2007	DBLP DOI BibTeX RDF
23	Andrea Asperti, Enrico Tassi	Higher order Proof Reconstruction from Paramodulation-Based Refutations: The Unit Equality Case.	Calculemus/MKM	2007	DBLP DOI BibTeX RDF
23	David Aspinall 0001, Daniel Winterstein, Christoph Lüth, Ahsan Fayyaz	Proof general in Eclipse: system and architecture overview.	ETX	2006	DBLP DOI BibTeX RDF	Eclipse
23	Andrew Cook, Andrew Ireland, Greg Michaelson, Norman Scaife	Discovering applications of higher order functions through proof planning.	Formal Aspects Comput.	2005	DBLP DOI BibTeX RDF
23	Changhua He, Mukund Sundararajan, Anupam Datta, Ante Derek, John C. Mitchell	A modular correctness proof of IEEE 802.11i and TLS.	CCS	2005	DBLP DOI BibTeX RDF	protocol composition logic, TLS, IEEE 802.11i
23	Florina Piroi, Temur Kutsia	The Theorema Environment for Interactive Proof Development.	LPAR	2005	DBLP DOI BibTeX RDF
23	Hongda Li 0001, Bao Li 0001	An Unbounded Simulation-Sound Non-interactive Zero-Knowledge Proof System for NP.	CISC	2005	DBLP DOI BibTeX RDF
23	David Pichardie	Modular Proof Principles for Parameterised Concretizations.	CASSIS	2005	DBLP DOI BibTeX RDF
23	Jan Krajícek	Combinatorics of first order structures and propositional proof systems.	Arch. Math. Log.	2004	DBLP DOI BibTeX RDF
23	J. Gregory Morrisett	Invited talk: what's the future for proof-carrying code?	PEPM	2004	DBLP DOI BibTeX RDF
23	Kazushige Terui	Proof Nets and Boolean Circuits.	LICS	2004	DBLP DOI BibTeX RDF