Search results for "Proof"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
16	Fabien Laguillaumie, Damien Vergnaud	On the Soundness of Restricted Universal Designated Verifier Signatures and Dedicated Signatures.	ISC	2007	DBLP DOI BibTeX RDF	Universal designated verifier signatures, zero-knowledge proof, Elgamal signatures
16	Gus Gutoski, John Watrous	Toward a general theory of quantum games.	STOC	2007	DBLP DOI BibTeX RDF	Choi-Jamiolkowski representation, quantum game theory, quantum strategies, interactive proof systems, coin-flipping
16	Michal Armoni	On the role of proofs in a course on design and analysis of algorithms.	ACM SIGCSE Bull.	2006	DBLP DOI BibTeX RDF	algorithms, correctness, proof
16	Oded Goldreich 0001, Madhu Sudan 0001	Locally testable codes and PCPs of almost-linear length.	J. ACM	2006	DBLP DOI BibTeX RDF	error-correcting codes, derandomization, probabilistically checkable proofs, Proof verification
16	Markus Schneider 0001, Thomas Behr	Topological relationships between complex spatial objects.	ACM Trans. Database Syst.	2006	DBLP DOI BibTeX RDF	9-intersection model, complex spatial data type, proof-by-constraint-and-drawing, topological cluster predicate, topological constraint rule, topological predicate group, Topological predicate
16	Alwen Tiu	A Local System for Intuitionistic Logic.	LPAR	2006	DBLP DOI BibTeX RDF	locality, proof theory, intuitionistic logic, intermediate logics, deep inference, calculus of structures
16	Sungduk Kim, Kyungjin Kim, Jaedong Jung, Dongho Won	An Efficient POP Protocol Based on the Signcryption Scheme for the WAP PKI.	EuroPKI	2006	DBLP DOI BibTeX RDF	proof of possession, signcryption, POP
16	Vijay Menon 0002, Neal Glew, Brian R. Murphy, Andrew McCreight, Tatiana Shpeisman, Ali-Reza Adl-Tabatabai, Leaf Petersen	A verifiable SSA program representation for aggressive compiler optimization.	POPL	2006	DBLP DOI BibTeX RDF	SSA formalization, check elimination, proof variables, safety dependences, typeability preservation, type systems, intermediate representations, typed intermediate languages
16	John Watrous	Zero-knowledge against quantum attacks.	STOC	2006	DBLP DOI BibTeX RDF	zero-knowledge proof systems, quantum cryptography
16	Zhong Shao, Valery Trifonov, Bratin Saha, Nikolaos Papaspyrou	A type system for certified binaries.	ACM Trans. Program. Lang. Syst.	2005	DBLP DOI BibTeX RDF	proof-preserving compilation, typed intermediate languages, Certified code
16	Zuhua Shao	Short Signature Scheme Based on Discrete Logarithms.	WAIM	2005	DBLP DOI BibTeX RDF	reductionist security proof, discrete logarithm, random oracle model, Short signature
16	Xinyu Feng 0001, Zhong Shao	Modular verification of concurrent assembly code with dynamic thread creation and termination.	ICFP	2005	DBLP DOI BibTeX RDF	concurrency verification, dynamic thread creation, proof-carrying code, rely-guarantee
16	Bor-Yuh Evan Chang, Adam Chlipala, George C. Necula, Robert R. Schneck	The open verifier framework for foundational verifiers.	TLDI	2005	DBLP DOI BibTeX RDF	language-based security, proof-carrying code, typed assembly language
16	Thomas Groß 0001, Birgit Pfitzmann, Ahmad-Reza Sadeghi	Proving a WS-federation passive requestor profile with a browser model.	SWS	2005	DBLP DOI BibTeX RDF	WS-federation passive requestor profile, WSFPI, security proof of protocols, single signon, web browser, web service security, identity federation
16	M. Jamshid Bagherzadeh, S. Arun-Kumar	Layered Clausal Resolution in the Multi-modal Logic of Beliefs and Goals.	LPAR	2004	DBLP DOI BibTeX RDF	proof method, multi-agent systems, resolution, belief revision, multi-modal logic
16	Vangelis Karatsiolis, Marcus Lippert, Alexander Wiesmaier	Using LDAP Directories for Management of PKI Processes.	EuroPKI	2004	DBLP DOI BibTeX RDF	Proof-of-Possession, Personal Security Environment, PKI, Public Key Infrastructure, LDAP, Directory Services, PSE, PoP
16	Jean-Christophe Filliâtre, Claude Marché	Multi-prover Verification of C Programs.	ICFEM	2004	DBLP DOI BibTeX RDF	pointer programs, formal verification and proof, Hoare logic, C programming language
16	Martin Hyland	Abstract Interpretation of Proofs: Classical Propositional Calculus.	CSL	2004	DBLP DOI BibTeX RDF	classical propositional calculus, category theory, proof theory
16	Pietro Di Gianantonio	Structures for Multiplicative Cyclic Linear Logic: Deepness vs Cyclicity.	CSL	2004	DBLP DOI BibTeX RDF	cyclic linear logic, linear logic, proof theory, Lambek calculus, calculus of structures
16	James Harland, David J. Pym	Resource-distribution via Boolean constraints.	ACM Trans. Comput. Log.	2003	DBLP DOI BibTeX RDF	Boolean constraints, Algebras, sequent calculus, substructural logics, proof-search, relevant logics
16	Amit Sahai, Salil P. Vadhan	A complete problem for statistical zero knowledge.	J. ACM	2003	DBLP DOI BibTeX RDF	Knowledge complexity, statistical difference, zero knowledge, proof systems
16	David Aspinall 0001, Adriana B. Compagnoni	Heap-Bounded Assembly Language.	J. Autom. Reason.	2003	DBLP DOI BibTeX RDF	proof-carrying code, typed assembly language
16	Eva Rose	Lightweight Bytecode Verification.	J. Autom. Reason.	2003	DBLP DOI BibTeX RDF	data flow analysis, proof-carrying code, bytecode verification
16	Byoungcheon Lee, Colin Boyd, Ed Dawson, Kwangjo Kim, Jeongmo Yang, Seungjae Yoo	Providing Receipt-Freeness in Mixnet-Based Voting Protocols.	ICISC	2003	DBLP DOI BibTeX RDF	Mixnet, Designated-verifier re-encryption proof, Tamper resistant randomizer, Electronic voting, Receipt-freeness, Re-encryption
16	Richard J. Fateman	High-level proofs of mathematical programs using automatic differentiation, simplification, and some common sense.	ISSAC	2003	DBLP DOI BibTeX RDF	Bessel, proof, differentiation, recurrence, sine
16	Jörg Rothe	Some facets of complexity theory and cryptography: A five-lecture tutorial.	ACM Comput. Surv.	2002	DBLP DOI BibTeX RDF	public-key cryptography, Complexity theory, one-way functions, interactive proof systems, zero-knowledge protocols
16	Stefan S. Dantchev	Resolution Width-Size Trade-offs for the Pigeon-Hole Principle.	CCC	2002	DBLP DOI BibTeX RDF	Pigeon-Hole Principle, Width-Size trade-off, Resolution, Propositional Proof Complexity
16	Amit Deshpande 0001, Rahul Jain 0001, Telikepalli Kavitha, Jaikumar Radhakrishnan, Satyanarayana V. Lokam	Better Lower Bounds for Locally Decodable Codes.	CCC	2002	DBLP DOI BibTeX RDF	Second Moment Method, Probabilistically Checkable Proof Systems, Error Correcting Codes, Pseudorandom Generators, Private Information Retrieval
16	Françoise Bellegarde, Christophe Darlot, Jacques Julliand, Olga Kouchnarenko	Reformulation: A Way to Combine Dynamic Properties and B Refinement.	FME	2001	DBLP DOI BibTeX RDF	Verification of PLTL properties, Combination of proof and model-checking, Refinement development
16	Albert Atserias	Improved Bounds on the Weak Pigeonhole Principle and Infinitely Many Primes from Weaker Axioms.	MFCS	2001	DBLP DOI BibTeX RDF	Weak Pigeonhole Principle, Proof Complexity, Bounded Arithmetic
16	Thomas Thomsen	Lambda-Search in Game Trees - with Application to Go.	Computers and Games	2000	DBLP DOI BibTeX RDF	binary tree search, threat-sequences, null-moves, proof-number search, abstract game-knowledge, Go block tactics
16	Reinhard Kahle, Thomas Studer	A Theory of Explicit Mathematics Equivalent to ID1.	CSL	2000	DBLP DOI BibTeX RDF	explicit mathematics, Proof theory, inductive definitions
16	Willy Susilo, Reihaneh Safavi-Naini, Josef Pieprzyk	RSA-Based Fail-Stop Signature Schemes.	ICPP Workshops	1999	DBLP DOI BibTeX RDF	Fail-Stop Signature Schemes, Proof of Forgery, RSA
16	Jon Whittle 0001, Alan Bundy, Richard J. Boulton, Helen Lowe	An ML Editor Based on Proofs-As-Programs.	ASE	1999	DBLP DOI BibTeX RDF	proofs-as-programs, termination proof, Functional programming
16	Sanjeev Arora, Shmuel Safra	Probabilistic Checking of Proofs: A New Characterization of NP.	J. ACM	1998	DBLP DOI BibTeX RDF	computations on polynomials and finite fields, proof checking, reducibility and completeness, trade-offs/relations among complexity measures, approximation algorithms, NP-completeness, error-correcting codes, hardness of approximations, probabilistic computation, interactive computation, complexity hierarchies
16	Gérard Le Lann	An analysis of the Ariane 5 flight 501 failure-a system engineering perspective.	ECBS	1997	DBLP DOI BibTeX RDF	Ariane 5 flight 501 failure, S/W Engineering, specification errors, application/environment requirements, on-board computing system, proof-based system engineering, systems engineering, system engineering
16	Savi Maharaj, Juan Bicarregui	On the Verification of VDM Specification and Refinement with PVS.	ASE	1997	DBLP DOI BibTeX RDF	VDM specification, VDM formal method, PVS theorem prover, VDM-SL specification translation, PVS specification language, transparent translation methods, specification type-checking, nontrivial validation conditions, abstract specification, shallow embedding technique, verification, formal specification, proof rules
16	Rakesh M. Verma	A Theory of Using History for Equational Systems with Applications.	J. ACM	1995	DBLP DOI BibTeX RDF	congruence-closure algorithm, rewrite system transformation, term rewrite systems, proof theory, equational logic
16	Ming-Yuan Zhu, Xiao-Bai Mo	Mechanical synthesis of a unification algorithm in PowerEpsilon.	COMPSAC	1995	DBLP DOI BibTeX RDF	PowerEpsilon, constructive type theory, proof development system, formal program development system, formal specification, specification, programming, theorem proving, programming theory, type theory, unification algorithm, mechanical synthesis
16	Henk Schepers, Jozef Hooman	Trace-Based Compositional Reasoning about Fault Tolerant Systems.	PARLE	1993	DBLP DOI BibTeX RDF	Compositional proof theory, fault hypothesis, relative network completeness, fault tolerance, verification, specification, safety, soundness
16	Juan Bicarregui, Brian Ritchie	Reasoning about VDM Developments using the VDM Support Tool in MURAL.	VDM Europe (1)	1991	DBLP DOI BibTeX RDF	integrated support environments, formal specification, formal methods, refinement, proof
16	Richard Gerber 0001, Insup Lee 0001	Specification and Analysis of Resource-Bound Real-Time Systems.	REX Workshop	1991	DBLP DOI BibTeX RDF	verification, Real-time, specification, programming languages, process algebras, configuration, proof systems
16	David Guaspari, Carla Marceau, Wolfgang Polak	Formal Verification of Ada Programs.	IEEE Trans. Software Eng.	1990	DBLP DOI BibTeX RDF	Penelope verification editor, formal basis, interactive development, logical soundness, interface languages, software engineering, Ada, program verification, correctness proof, prototype system, predicate transformers, Ada programs
16	Dipankar Sarkar 0001, S. C. De Sarkar	A Theorem Prover for Verifying Iterative Programs Over Integers.	IEEE Trans. Software Eng.	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
16	Bo Ingvar Sandén	Correction to "The Case for Electric Design of Real-Time Software''.	IEEE Trans. Software Eng.	1989	DBLP DOI BibTeX RDF	communication deadlocks detection, distributed scheme, distributed processing, correctness proof
16	William R. Bevier	Kit: A Study in Operating System Verification.	IEEE Trans. Software Eng.	1989	DBLP DOI BibTeX RDF	multitasking operating system kernel, machine language, uniprocessor von Neumann computer, conceptually distributed communicating processes, asynchronous devices, security-related results, supervisor mode, Boyer-Moore logic, Boyer-Moore theorem prover, verification, interface, message passing, theorem proving, program verification, operating systems (computers), multiprogramming, correctness proof, process scheduling, error handling, Kit
16	Liu Lingzhong	Comments on "A Distributed Scheme for Detecting Communication Deadlocks''.	IEEE Trans. Software Eng.	1989	DBLP DOI BibTeX RDF	communication deadlocks detection, distributed scheme, distributed processing, correctness proof
16	Werner Damm	A Microprogramming Logic.	IEEE Trans. Software Eng.	1988	DBLP DOI BibTeX RDF	microprogramming logic, syntax-directed proof system, horizontal computer architectures, clocked microarchitectures, axiomatic definition, microoperations, low-level parallelism, dynamic conflicts, specification, computer architecture, theorem proving, specification languages, architecture description language, formal logic, microprogramming, AADL, timing behavior
16	Gerard Tel	Assertional Verification of a Timer Based Protocol.	ICALP	1988	DBLP DOI BibTeX RDF	protocol skeleton, assertional proof, time, connection management, end-to-end protocol
15	Juan Chen 0002, Ravi Chugh, Nikhil Swamy	Type-preserving compilation of end-to-end verification of security enforcement.	PLDI	2010	DBLP DOI BibTeX RDF	bytecode languages, compilers, authorization, functional programming, information flow, dependent types, security type systems, mobile code security
15	Wei Zhang	On the decidability of open logic.	Sci. China Ser. F Inf. Sci.	2009	DBLP DOI BibTeX RDF	open logic, epistemic process, decidability
15	Yuan Dong, Shengyuan Wang, Liwei Zhang, Ping Yang	Modular Certification of Low-Level Intermediate Representation Programs.	COMPSAC (1)	2009	DBLP DOI BibTeX RDF
15	Stefan Hallerstede, Michael Leuschel	How to Explain Mistakes.	TFM	2009	DBLP DOI BibTeX RDF
15	Rajeev Goré, Linda Postniece, Alwen Tiu	Taming Displayed Tense Logics Using Nested Sequents with Deep Inference.	TABLEAUX	2009	DBLP DOI BibTeX RDF
15	Lionel Elie Mamane, Herman Geuvers, James McKinna	A Logically Saturated Extension of lambdaµµ.	Calculemus/MKM	2009	DBLP DOI BibTeX RDF
15	Chunming Tang 0003, Dingyi Pei, Xiaofeng Wang, Zhuojun Liu	Delegateable signatures based on non-interactive witness indistinguishable and non-interactive witness hiding proofs.	Sci. China Ser. F Inf. Sci.	2008	DBLP DOI BibTeX RDF	delegateable signature, non-interactive witness indistinguishable, non-interactive witness hiding, ?-protocol, non-interactive zero-knowledge
15	Josef Urban, Geoff Sutcliffe	ATP-based Cross-Verification of Mizar Proofs: Method, Systems, and First Experiments.	Math. Comput. Sci.	2008	DBLP DOI BibTeX RDF	verification, automated reasoning, Formalized mathematics
15	Gerard R. Renardel de Lavalette, Barteld P. Kooi, Rineke Verbrugge	Strong Completeness and Limited Canonicity for PDL.	J. Log. Lang. Inf.	2008	DBLP DOI BibTeX RDF	Canonical model, Model disharmony, Propositional dynamic logic, Strong completeness
15	Jessica Chang, Thomas Erlebach, Renars Gailis, Samir Khuller	Broadcast scheduling: algorithms and complexity.	SODA	2008	DBLP BibTeX RDF
15	Carsten Schürmann 0001, Jeffrey Sarnat	Structural Logical Relations.	LICS	2008	DBLP DOI BibTeX RDF	Twelf, Normalization, Logical Frameworks, Cut-Elimination, Logical Relations
15	Kurt Dietrich	A Secure and Reliable Platform Configuration Change Reporting Mechanism for Trusted Computing Enhanced Secure Channels.	ICYCS	2008	DBLP DOI BibTeX RDF
15	Hovav Shacham, Brent Waters	Compact Proofs of Retrievability.	ASIACRYPT	2008	DBLP DOI BibTeX RDF
15	Shafi Goldwasser, Yael Tauman Kalai, Guy N. Rothblum	Delegating computation: interactive proofs for muggles.	STOC	2008	DBLP DOI BibTeX RDF	muggles, delegation, interactive proofs
15	Heidar Pirzadeh, Danny Dubé	Encoding the Program Correctness Proofs as Programs in PCC Technology.	PST	2008	DBLP DOI BibTeX RDF
15	David Aspinall 0001, Ewen Denney, Christoph Lüth	A Tactic Language for Hiproofs.	AISC/MKM/Calculemus	2008	DBLP DOI BibTeX RDF
15	Sunae Seo, Hongseok Yang, Kwangkeun Yi, Taisook Han	Goal-directed weakening of abstract interpretation results.	ACM Trans. Program. Lang. Syst.	2007	DBLP DOI BibTeX RDF	static analysis, Abstract interpretation, program verification, Hoare logic, backward analysis
15	Benjamin Grégoire, Jorge Luis Sacchini	Combining a Verification Condition Generator for a Bytecode Language with Static Analyses.	TGC	2007	DBLP DOI BibTeX RDF
15	Josef Urban, Geoff Sutcliffe	ATP Cross-Verification of the Mizar MPTP Challenge Problems.	LPAR	2007	DBLP DOI BibTeX RDF
15	Gerwin Klein, Tobias Nipkow	A machine-checked model for a Java-like language, virtual machine, and compiler.	ACM Trans. Program. Lang. Syst.	2006	DBLP DOI BibTeX RDF	Java, theorem proving, operational semantics
15	Michael Backes 0001, Birgit Pfitzmann	On the Cryptographic Key Secrecy of the Strengthened Yahalom Protocol.	SEC	2006	DBLP DOI BibTeX RDF
15	Tetsuo Ida, Hidekazu Takahashi, Mircea Marin, Fadoua Ghourabi, Asem Kasem	Computational Construction of a Maximum Equilateral Triangle Inscribed in an Origami.	ICMS	2006	DBLP DOI BibTeX RDF
15	Yael Tauman Kalai, Ran Raz	Succinct Non-Interactive Zero-Knowledge Proofs with Preprocessing for LOGSNP.	FOCS	2006	DBLP DOI BibTeX RDF
15	Frédéric Besson	Fast Reflexive Arithmetic Tactics the Linear Case and Beyond.	TYPES	2006	DBLP DOI BibTeX RDF
15	Olaf Beyersdorff	Tuples of Disjoint NP-Sets.	CSR	2006	DBLP DOI BibTeX RDF
15	Arist Kojevnikov, Alexander S. Kulikov	Complexity of Semialgebraic Proofs with Restricted Degree of Falsity.	SAT	2006	DBLP DOI BibTeX RDF
15	Daniel Kroening, Natasha Sharygina	Approximating Predicate Images for Bit-Vector Logic.	TACAS	2006	DBLP DOI BibTeX RDF
15	DoRon B. Motter, Jarrod A. Roy, Igor L. Markov	Resolution cannot polynomially simulate compressed-BFS.	Ann. Math. Artif. Intell.	2005	DBLP DOI BibTeX RDF
15	Elaine Pimentel, Dale Miller 0001	On the Specification of Sequent Systems.	LPAR	2005	DBLP DOI BibTeX RDF
15	Susumu Hayashi	Can Proofs Be Animated By Games?	TLCA	2005	DBLP DOI BibTeX RDF
15	Ran Raz	Quantum Information and the PCP Theorem.	FOCS	2005	DBLP DOI BibTeX RDF
15	Amitabh Saxena, Ben Soh, Dimitri Zantidis	A Digital Cash Protocol Based on Additive Zero Knowledge.	ICCSA (3)	2005	DBLP DOI BibTeX RDF
15	Aaron Stump, Li-Yang Tan	The Algebra of Equality Proofs.	RTA	2005	DBLP DOI BibTeX RDF
15	Jürgen Schmidhuber	Completely Self-referential Optimal Reinforcement Learners.	ICANN (2)	2005	DBLP DOI BibTeX RDF
15	David Aspinall 0001, Kenneth MacKenzie	Mobile Resource Guarantees and Policies.	CASSIS	2005	DBLP DOI BibTeX RDF
15	Serge Autexier, Armin Fiedler	Textbook Proofs Meet Formal Logic - The Problem of Underspecification and Granularity.	MKM	2005	DBLP DOI BibTeX RDF
15	Matthias Baaz, Stefan Hetzl, Alexander Leitsch, Clemens Richter, Hendrik Spohr	Cut-Elimination: Experiments with CERES.	LPAR	2004	DBLP DOI BibTeX RDF
15	Konstantine Arkoudas, Karen Zee, Viktor Kuncak, Martin C. Rinard	Verifying a File System Implementation.	ICFEM	2004	DBLP DOI BibTeX RDF
15	Leslie Ann Goldberg, Russell A. Martin, Mike Paterson	trong Spatial Mixing for Lattice Graphs with Fewer Colours.	FOCS	2004	DBLP DOI BibTeX RDF
15	Fredrik Lindblad, Marcin Benke	A Tool for Automated Theorem Proving in Agda.	TYPES	2004	DBLP DOI BibTeX RDF
15	Jonathan Katz, Rafail Ostrovsky, Michael O. Rabin	Identity-Based Zero Knowledge.	SCN	2004	DBLP DOI BibTeX RDF
15	Michael Backes 0001, Birgit Pfitzmann, Michael Waidner	Justifying a Dolev-Yao Model Under Active Attacks.	FOSAD	2004	DBLP DOI BibTeX RDF
15	Chris Marriott, John Watrous	Quantum Arthur-Merlin Games.	CCC	2004	DBLP DOI BibTeX RDF
15	Martín Nordio, Ricardo H. Medel, Francisco Bavera, Jorge Aguirre, Gabriel Baum	A Framework for Execution of Secure Mobile Code based on Static Analysis.	SCCC	2004	DBLP DOI BibTeX RDF
15	Daniele Micciancio, Erez Petrank	Simulatable Commitments and Efficient Concurrent Zero-Knowledge.	EUROCRYPT	2003	DBLP DOI BibTeX RDF
15	Huaming Zhang, Xin He	On Even Triangulations of 2-Connected Embedded Graphs.	COCOON	2003	DBLP DOI BibTeX RDF
15	Chris Hankin, Rajagopal Nagarajan, Prahladavaradan Sampath	Flow Analysis: Games and Nets.	The Essence of Computation	2002	DBLP DOI BibTeX RDF
15	Dario Catalano, Phong Q. Nguyen, Jacques Stern	The Hardness of Hensel Lifting: The Case of RSA and Discrete Logarithm.	ASIACRYPT	2002	DBLP DOI BibTeX RDF	Paillier, Hensel, One-wayness, RSA, Lattice, Discrete logarithm, Public-key
15	Dima Grigoriev, Edward A. Hirsch, Dmitrii V. Pasechnik	Complexity of Semi-algebraic Proofs.	STACS	2002	DBLP DOI BibTeX RDF
15	Elliot Anshelevich, David Kempe 0001, Jon M. Kleinberg	Stability of load balancing algorithms in dynamic adversarial systems.	STOC	2002	DBLP DOI BibTeX RDF
15	Maurice Herlihy, Sergio Rajsbaum, Mark R. Tuttle	A New Synchronous Lower Bound for Set Agreement.	DISC	2001	DBLP DOI BibTeX RDF