Search results for "Proof"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
23	Guillaume Lussier, Hélène Waeselynck, Karim Guennoun	Proof-Guided Testing: An Experimental Study.	COMPSAC	2004	DBLP DOI BibTeX RDF
23	J. Gregory Morrisett	Invited talk: what's the future for proof-carrying code?	PPDP	2004	DBLP DOI BibTeX RDF
23	Michael Backes 0001	A Cryptographically Sound Dolev-Yao Style Security Proof of the Otway-Rees Protocol.	ESORICS	2004	DBLP DOI BibTeX RDF
23	Dominic J. D. Hughes, Rob J. van Glabbeek	Proof Nets for Unit-free Multiplicative-Additive Linear Logic (Extended abstract).	LICS	2003	DBLP DOI BibTeX RDF
23	Nadeem Abdul Hamid, Zhong Shao, Valery Trifonov, Stefan Monnier, Zhaozhong Ni	A Syntactic Approach to Foundational Proof-Carrying Code.	LICS	2002	DBLP DOI BibTeX RDF
23	Héctor Ruíz Barradas, Didier Bert	Specification and Proof of Liveness Properties under Fairness Assumptions in B Event Systems.	IFM	2002	DBLP DOI BibTeX RDF
23	Amir Pnueli, Yonit Kesten	A Deductive Proof System for CTL.	CONCUR	2002	DBLP DOI BibTeX RDF
23	George C. Necula, Peter Lee 0001	Proof Generation in the Touchstone Theorem Prover.	CADE	2000	DBLP DOI BibTeX RDF
23	Jean-Marc Andreoli, Roberto Maieli	Fucusing and Proof-Nets in Linear and Non-commutative Logic.	LPAR	1999	DBLP DOI BibTeX RDF
23	Anna Mikhajlova, Joakim von Wright	Proving Isomorphism of First-Order Logic Proof Systems in HOL.	TPHOLs	1998	DBLP DOI BibTeX RDF
23	Katherine A. Eastaughffe, Maris A. Ozols, Anthony Cant	Proof Tactics for a Theory of State Machines in a Graphical Environment.	CADE	1997	DBLP DOI BibTeX RDF
23	Lena Magnusson	An Algorithm for Checking Incomplete Proof Objects in Type Theory with Localization and Unification.	TYPES	1995	DBLP DOI BibTeX RDF
23	Naima Brown, Dominique Méry	A Proof Environment for Concurrent Programs.	FME	1993	DBLP DOI BibTeX RDF	formal specifications, concurrency, program verification, Automated theorem proving, B, Unity
23	Matthew Hennessy, Huimin Lin	Proof Systems for Message-Passing Process Algebras.	CONCUR	1993	DBLP DOI BibTeX RDF
23	Toshiya Itoh, Masafumi Hoshi, Shigeo Tsujii	A Low Communication Competitive Interactive Proof System for Promised Quadratic Residuosity.	CRYPTO	1993	DBLP DOI BibTeX RDF
23	Chaosheng Shu, Tsutomu Matsumoto, Hideki Imai	A Multi-Purpose Proof System - for Identity and Membership Proofs.	ASIACRYPT	1991	DBLP DOI BibTeX RDF
23	Paul Y. Gloess	An Experiment with the Boyer-Moore Theorem Prover: A Proof of the Correctness of a Simple Parser of Expressions.	CADE	1980	DBLP DOI BibTeX RDF
23	Stephan Merz	Proofs and Proof Certification in the TLA+ Proof System.	PxTP	2012	DBLP BibTeX RDF
23	Frédéric Besson, Pierre-Emmanuel Cornilleau, David Pichardie	A Nelson-Oppen based Proof System using Theory Specific Proof Systems.	PxTP	2011	DBLP BibTeX RDF
23	Wilfried Buchholz	Explaining Gentzen's Consistency Proof within Infinitary Proof Theory.	Kurt Gödel Colloquium	1997	DBLP DOI BibTeX RDF
23	Iddo Bentov, Charles Lee, Alex Mizrahi, Meni Rosenfeld	Proof of Activity: Extending Bitcoin's Proof of Work via Proof of Stake [Extended Abstract]y.	SIGMETRICS Perform. Evaluation Rev.	2014	DBLP DOI BibTeX RDF
23	Iddo Bentov, Charles Lee, Alex Mizrahi, Meni Rosenfeld	Proof of Activity: Extending Bitcoin's Proof of Work via Proof of Stake.	IACR Cryptol. ePrint Arch.	2014	DBLP BibTeX RDF
23	Marianne Winslett	Moshe Vardi speaks out on the proof, the whole proof, and nothing but the proof.	SIGMOD Rec.	2006	DBLP DOI BibTeX RDF
22	Michael J. Butler, Divakar Yadav	An incremental development of the Mondex system in Event-B.	Formal Aspects Comput.	2008	DBLP DOI BibTeX RDF	Mechanical proof, Methodological guidelines, Refinement, System design, Event-B
22	Aytekin Vargun, David R. Musser	Code-carrying theory.	SAC	2008	DBLP DOI BibTeX RDF	secure code delivery, correctness, proof-carrying code, memory safety
22	Adam Chlipala	A certified type-preserving compiler from lambda calculus to assembly language.	PLDI	2007	DBLP DOI BibTeX RDF	denotational semantics, dependent types, compiler verification, interactive proof assistants
22	Josef Urban	MPTP 0.2: Design, Implementation, and Initial Experiments.	J. Autom. Reason.	2006	DBLP DOI BibTeX RDF	MPTP, Mizar, ATP, MPA, re-proving, proof discovery, MML
22	Zhaozhong Ni, Zhong Shao	Certified assembly programming with embedded code pointers.	POPL	2006	DBLP DOI BibTeX RDF	embedded code pointers, hoare logic, proof-carrying code, higher-order functions
22	Christian Urban, Stefan Berghofer	A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL.	IJCAR	2006	DBLP DOI BibTeX RDF	Lambda-calculus, proof assistants, nominal logic, primitive recursion
22	Tie Hou	Coinductive Proofs for Basic Real Computation.	CiE	2006	DBLP DOI BibTeX RDF	Real computation, Coinductive proof, Signed digit streams, Minlog, Computability
22	Jakob Nordström	Narrow proofs may be spacious: separating space and width in resolution.	STOC	2006	DBLP DOI BibTeX RDF	pebbling contradiction, lower bound, resolution, space, separation, proof complexity, width, pebble game
22	Bruno Mermet, Dominique Fournier	Variant Extensions to Prove MAS Behaviours.	AIMSA	2004	DBLP DOI BibTeX RDF	prey-predator, multi-agent system, proof, variant
22	Byoungcheon Lee, Kwangjo Kim	Receipt-Free Electronic Voting Scheme with a Tamper-Resistant Randomizer.	ICISC	2002	DBLP DOI BibTeX RDF	tamper-resistant randomizer, divertible zero-knowledge proof, Electronic voting, receipt-freeness
22	Ben L. Di Vito	High-automation proofs for properties of requirements models.	Int. J. Softw. Tools Technol. Transf.	2000	DBLP DOI BibTeX RDF	Avionics software, Proof strategies, Formal methods, Theorem proving, Requirements analysis
22	H. Conrad Cunningham, Gruia-Catalin Roman	A UNITY-Style Programming Logic for Shared Dataspace Programs.	IEEE Trans. Parallel Distributed Syst.	1990	DBLP DOI BibTeX RDF	UNITY-style programming logic, shared dataspace programs, program verification, Swarm, proof system, program correctness
22	Shmuel Katz, Doron A. Peled	An efficient verification method for parallel and distributed programs.	REX Workshop	1988	DBLP DOI BibTeX RDF	Proof lattices, Verification, Temporal logic, Partial order semantics, Execution sequences
21	Olaf Beyersdorff, Sebastian Müller 0003	Does Advice Help to Prove Propositional Tautologies?	SAT	2009	DBLP DOI BibTeX RDF
21	Eli Ben-Sasson, Jakob Nordström	Short Proofs May Be Spacious: An Optimal Separation of Space and Length in Resolution.	FOCS	2008	DBLP DOI BibTeX RDF
21	Omer Bar-Ilan, Oded Fuhrmann, Shlomo Hoory, Ohad Shacham, Ofer Strichman	Linear-Time Reductions of Resolution Proofs.	Haifa Verification Conference	2008	DBLP DOI BibTeX RDF
21	Christian Glaßer, Alan L. Selman, Liyu Zhang	The Informational Content of Canonical Disjoint NP-Pairs.	COCOON	2007	DBLP DOI BibTeX RDF
21	Marc Bezem, Thierry Coquand	Automating Coherent Logic.	LPAR	2005	DBLP DOI BibTeX RDF
21	James Brotherston	Cyclic Proofs for First-Order Logic with Inductive Definitions.	TABLEAUX	2005	DBLP DOI BibTeX RDF
21	Clemens Grabmayer	Using Proofs by Coinduction to Find "Traditional" Proofs.	CALCO	2005	DBLP DOI BibTeX RDF
21	Lars-Åke Fredlund, Dilian Gurov, Thomas Noll 0001, Mads Dam, Thomas Arts, Gennady Chugunov	A verification tool for ERLANG.	Int. J. Softw. Tools Technol. Transf.	2003	DBLP DOI BibTeX RDF	Formal methods, Theorem proving, Software verification
21	W. O. David Griffioen, Marieke Huisman	A Comparison of PVS and Isabelle/HOL.	TPHOLs	1998	DBLP DOI BibTeX RDF
21	Myla Archer, Constance L. Heitmeyer	Human-Style Theorem Proving Using PVS.	TPHOLs	1997	DBLP DOI BibTeX RDF
21	Ivan Damgård, Oded Goldreich 0001, Tatsuaki Okamoto, Avi Wigderson	Honest Verifier vs Dishonest Verifier in Public Coin Zero-Knowledge Proofs.	CRYPTO	1995	DBLP DOI BibTeX RDF
21	Amy P. Felty, Douglas J. Howe	Generalization and Reuse of Tactic Proofs.	LPAR	1994	DBLP DOI BibTeX RDF
21	Toshiya Itoh, Kouichi Sakurai, Hiroki Shizuya	Any Language in IP Has a Divertable ZKIP.	ASIACRYPT	1991	DBLP DOI BibTeX RDF
21	Gregory A. Frascadore	Combining explanation based generalization with the learning of macro operators (abstract only).	ACM Conference on Computer Science	1987	DBLP DOI BibTeX RDF
21	Stephen D. Brookes	On the Axiomatic Treatment of Concurrency.	Seminar on Concurrency	1984	DBLP DOI BibTeX RDF
21	Vaughan R. Pratt	Axioms or Algorithms.	MFCS	1979	DBLP DOI BibTeX RDF
21	Balaji Venkatachalam	Software Watermarking as a Proof of Identity: A Study of Zero Knowledge Proof Based Software Watermarking.	IWDW	2005	DBLP DOI BibTeX RDF
21	Luís Caires, Luís Monteiro	Proof Net Semantics of Proof Search Computation.	ALP/HOA	1997	DBLP DOI BibTeX RDF
21	Frédéric Vogels, Bart Jacobs 0002, Frank Piessens	A machine-checked soundness proof for an efficient verification condition generator.	SAC	2010	DBLP DOI BibTeX RDF	soundness proof, verification conditions
21	Greg Restall	Truth Values and Proof Theory.	Stud Logica	2009	DBLP DOI BibTeX RDF	Completeness, Modal Logic, Proof, Sequent Calculus, Intuitionistic Logic, Truth Value
21	Don Blaheta	A visual proof of amortised-linear resizable arrays.	ITiCSE	2009	DBLP DOI BibTeX RDF	amortised analysis, visual proof
21	Benjamin C. Pierce	Lambda, the ultimate TA: using a proof assistant to teach programming language foundations.	ICFP	2009	DBLP DOI BibTeX RDF	programming languages, pedagogy, proof assistants
21	Dane Hamilton, Katina Michael, Samuel Fosso Wamba	Using RFID to Overcome Inventory Control Challenges: A Proof of Concept.	UIC	2009	DBLP DOI BibTeX RDF	simulation, business process, RFID technology, proof of concept
21	Arjeh M. Cohen, Jan Willem Knopper, Scott H. Murray	Automatic Proof of Graph Nonisomorphism.	Math. Comput. Sci.	2008	DBLP DOI BibTeX RDF	automatic proof generation, Graphs, groups, graph isomorphism
21	Amine Chaieb, Tobias Nipkow	Proof Synthesis and Reflection for Linear Arithmetic.	J. Autom. Reason.	2008	DBLP DOI BibTeX RDF	Proof synthesis, Linear arithmetic, Reflection
21	Chunming Tang 0003, Dingyi Pei, Zheng-an Yao	5-Round Computational Zero-Knowledge Proof with Negligible Error Probability for Any NP from Any One-Way Permutation.	ISECS	2008	DBLP DOI BibTeX RDF	computational zero-knowledge proof, perfectly hiding commitment, one-way permutation
21	Paulin Jacobé de Naurois, Virgile Mogbil	Correctness of Multiplicative Additive Proof Structures is NL-Complete.	LICS	2008	DBLP DOI BibTeX RDF	Correctness Criterion, Multiplicative Additive Linear Logic, NL-completness, Computational Complexity, proof-nets
21	Luca Roversi, Luca Vercelli	Some Complexity and Expressiveness Results on Multimodal and Stratified Proof Nets.	TYPES	2008	DBLP DOI BibTeX RDF	Structural Proof-theory, Polynomial Time Computations, Linear Logic, Implicit Computational Complexity
21	Nadir Weibel, Adriana Ispas, Beat Signer, Moira C. Norrie	Paperproof: a paper-digital proof-editing system.	CHI Extended Abstracts	2008	DBLP DOI BibTeX RDF	digital pen and paper, document life-cycle, proof-editing, interactive paper, gesture-based interface
21	JungHoon Ha, Sang-Jae Moon, Jianying Zhou 0001, JaeCheol Ha	A New Formal Proof Model for RFID Location Privacy.	ESORICS	2008	DBLP DOI BibTeX RDF	formal proof model, location privacy, RFID security
21	Slawomir Grzonkowski, Wojciech Zaremba, Maciej Zaremba, Bill McDaniel	Extending web applications with a lightweight zero knowledge proof authentication.	CSTST	2008	DBLP DOI BibTeX RDF	web 2.0 authentication, protocols, web 2.0, password, graph isomorphism, zero knowledge proof
21	Paul Piwek	Meaning and Dialogue Coherence: A Proof-theoretic Investigation.	J. Log. Lang. Inf.	2007	DBLP DOI BibTeX RDF	Multi-agent Inference, Proof-theoretic semantics, Coherence, Natural deduction, Dialogue modelling
21	Nadeem Abdul Hamid	Integrating a certified memory management runtime with proof-carrying code.	SAC	2007	DBLP DOI BibTeX RDF	certified memory management, proof-carrying code
21	William H. Winsborough, Anna Cinzia Squicciarini, Elisa Bertino	Information carrying identity proof trees.	WPES	2007	DBLP DOI BibTeX RDF	identity proof, identity provenance, validation
21	Nikita Borisov, Kazuhiro Minami	Single-bit re-encryption with applications to distributed proof systems.	WPES	2007	DBLP DOI BibTeX RDF	commutative encryption, distributed proof systems, goldwasser-micali, covert channels, re-encryption
21	Akihiro Yamamura, Takashi Kurokawa 0001, Junji Nakazato	Threshold Anonymous Group Identification and Zero-Knowledge Proof.	ACISP	2007	DBLP DOI BibTeX RDF	t-out-of-m Anonymous Group Identification, Non-singular Matrix, Zero-Knowledge Proof
21	David Ginat, Michal Armoni	Reversing: an essential heuristic in program and proof design.	SIGCSE	2006	DBLP DOI BibTeX RDF	proof design, reverse thinking, program design
21	Ygal Bendavid, Samuel Fosso Wamba, Louis A. Lefebvre	Proof of concept of an RFID-enabled supply chain in a B2B e-commerce environment.	ICEC	2006	DBLP DOI BibTeX RDF	process optimization, utility industry, RFID, ERP, supply chain, warehouse, proof of concept
21	Sébastien Kunz-Jacques, Gwenaëlle Martinet, Guillaume Poupard, Jacques Stern	Cryptanalysis of an Efficient Proof of Knowledge of Discrete Logarithm.	Public Key Cryptography	2006	DBLP DOI BibTeX RDF	discrete logarithm, proof of knowledge, Public key cryptanalysis
21	Roberto Maieli, Quintijn Puite	Modularity of proof-nets.	Arch. Math. Log.	2005	DBLP DOI BibTeX RDF	Weak (or linear) distributivity, Modules, Linear logic, Proof-nets
21	Nuno Amálio, Susan Stepney, Fiona Polack	Formal Proof from UML Models.	ICFEM	2004	DBLP DOI BibTeX RDF	UML, Z, consistency checking, formal proof, model analysis
21	Corneliu Popeea, Wei-Ngan Chin	A type system for resource protocol verification and its correctness proof.	PEPM	2004	DBLP DOI BibTeX RDF	dependent type system, resource specification, protocol verification, correctness proof, path-sensitive analysis
21	Frederick W. Chapman	An elementary algorithm for the automatic derivation and proof of tensor product identities via computer algebra.	ISSAC	2003	DBLP DOI BibTeX RDF	Taylor interpolation, asymptotic splitting operator, automatic derivation, automatic proof, binormal forms, bivariate identities, characteristic cauchy problem, dual asymptotic expansions, homogeneous hyperbolic eigenproblem, hyperbolic eigenfunction, symmetries, maple, computer algebra, differential equations, tensor products, lie groups
21	Cynthia Dwork, Larry J. Stockmeyer	2-round zero knowledge and proof auditors.	STOC	2002	DBLP DOI BibTeX RDF	advice bound, timed protocol, zap, cryptography, zero knowledge, interactive proof systems
21	Shuzhen Dong, Qiwen Xu, Naijun Zhan	A Formal Proof of the Rate Monotonic Scheduler.	RTCSA	1999	DBLP DOI BibTeX RDF	Scheduling, Logic, Duration Calculus, Formal Proof, Feasibility
21	Frank S. de Boer	A Proof System for the Language POOL.	REX Workshop	1990	DBLP DOI BibTeX RDF	partial correctness, completeness, Object, soundness, Hoare-logic, pointers, proof-system, rendezvous, object-creation
21	George Peterka, Tadao Murata	Proof Procedure and Answer Extraction in Petri Net Model of Logic Programs.	IEEE Trans. Software Eng.	1989	DBLP DOI BibTeX RDF	proof procedure, Horn clause subset, firing sequence, goal transition, Petri nets, logic programs, logic programming, theorem proving, programming theory, Petri net model, first-order predicate logic, answer extraction
20	Lilian Burdy, Antoine Requet, Jean-Louis Lanet	Java Applet Correctness: A Developer-Oriented Approach.	FME	2003	DBLP DOI BibTeX RDF	Proof User Interface, Java, Correctness Proof
20	Samuel R. Buss, Dima Grigoriev, Russell Impagliazzo, Toniann Pitassi	Linear Gaps Between Degrees for the Polynomial Calculus Modulo Distinct Primes (Abstract).	CCC	1999	DBLP DOI BibTeX RDF	counting principles, graph tautologies, algebraic proof systems, binomial proofs, Nullstellensatz proofs, polynomial calculus proofs, propositional logic, Proof complexity
20	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
20	David A. McAllester	Automatic Recognition of Tractability in Inference Relations.	J. ACM	1993	DBLP DOI BibTeX RDF	machine inference, theorem proving, polynomial-time algorithm, automated reasoning, inference rules, proof theory, proof systems, mechanical verification
20	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
20	Paola Bruscoli, Alessio Guglielmi	On the proof complexity of deep inference.	ACM Trans. Comput. Log.	2009	DBLP DOI BibTeX RDF	Frege systems, Statman tautologies, Analyticity, deep inference, calculus of structures
20	Rajeev Goré	Machine Checking Proof Theory: An Application of Logic to Logic.	ICLA	2009	DBLP DOI BibTeX RDF
20	William Lovas, Frank Pfenning	Refinement Types as Proof Irrelevance.	TLCA	2009	DBLP DOI BibTeX RDF
20	Zhiyao Liang, Rakesh M. Verma	Correcting and Improving the NP Proof for Cryptographic Protocol Insecurity.	ICISS	2009	DBLP DOI BibTeX RDF	insecurity, Cryptographic protocols, secrecy, NP
20	Allen Van Gelder	Improved Conflict-Clause Minimization Leads to Improved Propositional Proof Traces.	SAT	2009	DBLP DOI BibTeX RDF
20	Mihir Bellare, Thomas Ristenpart	Simulation without the Artificial Abort: Simplified Proof and Improved Concrete Security for Waters' IBE Scheme.	EUROCRYPT	2009	DBLP DOI BibTeX RDF
20	Tsz Hon Yuen, Qiong Huang 0001, Yi Mu 0001, Willy Susilo, Duncan S. Wong, Guomin Yang	Efficient Non-interactive Range Proof.	COCOON	2009	DBLP DOI BibTeX RDF
20	Jacques Patarin	A Proof of Security in O(2n) for the Xor of Two Random Permutations.	ICITS	2008	DBLP DOI BibTeX RDF	security beyond the birthday bound, Luby-Rackoff backwards, Pseudorandom functions, pseudorandom permutations
20	Olivier Delande, Dale Miller 0001	A Neutral Approach to Proof and Refutation in MALL.	LICS	2008	DBLP DOI BibTeX RDF	neutral approach, linear logic, game semantics
20	Vincent Conitzer	Anonymity-Proof Voting Rules.	WINE	2008	DBLP DOI BibTeX RDF
20	Toru Ueda, Tsuyoshi Hashimoto, Junichi Hashimoto, Hiroyuki Iida	Weak Proof-Number Search.	Computers and Games	2008	DBLP DOI BibTeX RDF
20	Stefan Hallerstede	On the Purpose of Event-B Proof Obligations.	ABZ	2008	DBLP DOI BibTeX RDF