Search results for "Theorem-Proving"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
21	Hongbo Li 0012, Lei Huang	Complex brackets, balanced complex differences, and applications in symbolic geometric computing.	ISSAC	2008	DBLP DOI BibTeX RDF	bracket algebra, complex numbers method, graph theory, theorem proving, geometric algebra
21	Viorica Sofronie-Stokkermans	On unification for bounded distributive lattices.	ACM Trans. Comput. Log.	2007	DBLP DOI BibTeX RDF	decision procedures for the positive theory, Theorem proving, unification, distributive lattices, SAT solving
21	Clark W. Barrett, Leonardo Mendonça de Moura, Aaron Stump	Design and results of the 2nd annual satisfiability modulo theories competition (SMT-COMP 2006).	Formal Methods Syst. Des.	2007	DBLP DOI BibTeX RDF	Competition, Decision procedures, Automated theorem proving, SMT, Satisfiability modulo theories
21	Greg Bronevetsky, Bronis R. de Supinski	Complete Formal Specification of the OpenMP Memory Model.	Int. J. Parallel Program.	2007	DBLP DOI BibTeX RDF	parallel programming, theorem proving, OpenMP, formal systems
21	Swen Jacobs, Uwe Waldmann	Comparing Instance Generation Methods for Automated Reasoning.	J. Autom. Reason.	2007	DBLP DOI BibTeX RDF	disconnection calculus, primal partial instantiation, resolution-based instance generation, theorem proving, automated reasoning
21	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
21	Julien Narboux	A Graphical User Interface for Formal Proofs in Geometry.	J. Autom. Reason.	2007	DBLP DOI BibTeX RDF	Interface, Geometry, Automated theorem proving, Theorem prover, Proof assistant, Coq, Dynamic geometry
21	Alberto Ciaffaglione, Luigi Liquori, Marino Miculan	Reasoning about Object-based Calculi in (Co)Inductive Type Theory and the Theory of Contexts.	J. Autom. Reason.	2007	DBLP DOI BibTeX RDF	Functional and imperative object-calculi, Logical foundations of programming, Coinductive type theories, Logical frameworks, Interactive theorem proving
21	Reinhold Letz, Gernot Stenz	The Disconnection Tableau Calculus.	J. Autom. Reason.	2007	DBLP DOI BibTeX RDF	disconnection tableaux, theorem proving
21	Wenjun Wu 0003, Xiao-Shan Gao	Mathematics mechanization and applications after thirty years.	Frontiers Comput. Sci. China	2007	DBLP DOI BibTeX RDF	mathematics mechanization, characteristic set method, automated theorem discovering, symbolic equation solving, intelligent computer-aided design, computer vision, robotics, automated theorem proving, computer aided geometric design
21	Damián Barsotti, Leonor Prensa Nieto, Alwen Tiu	Verification of clock synchronization algorithms: experiments on a combination of deductive tools.	Formal Aspects Comput.	2007	DBLP DOI BibTeX RDF	Combination of deductive tools, Verification, Theorem proving, Clock synchronization
21	Paul Curzon, Rimvydas Ruksenas, Ann Blandford	An approach to formal verification of human-computer interaction.	Formal Aspects Comput.	2007	DBLP DOI BibTeX RDF	Formal cognitive architecture, Formal verification, Theorem proving, Interactive systems, Human error
21	Chris Lesniewski-Laas, Bryan Ford, Jacob Strauss, Robert Tappan Morris, M. Frans Kaashoek	Alpaca: extensible authorization for distributed services.	CCS	2007	DBLP DOI BibTeX RDF	security, cryptography, authorization, theorem-proving, logic
21	Shoichi Morimoto, Shinjiro Shigematsu, Yuichi Goto, Jingde Cheng	Formal verification of security specifications with common criteria.	SAC	2007	DBLP DOI BibTeX RDF	ISO/IEC 15408, theorem-proving, Z notation
21	Yongjian Li	Mechanized proofs for the parameter abstraction and guard strengthening principle in parameterized verification of cache coherence protocols.	SAC	2007	DBLP DOI BibTeX RDF	parameterized verification, theorem proving, symmetry
21	Harvey Tuch, Gerwin Klein, Michael Norrish	Types, bytes, and separation logic.	POPL	2007	DBLP DOI BibTeX RDF	C, separation logic, interactive theorem proving
21	Leo Freitas, Jim Woodcock 0001	Proving Theorems About JML Classes.	Formal Methods and Hybrid Real-Time Systems	2007	DBLP DOI BibTeX RDF	Grand Challenge in Verified Software, Java Collections Framework, Java HashMap class, linking theories, Z/Eves, formal specification, Z, software verification, JML, Java Modeling Language, mechanical theorem proving, Verified Software Repository
21	Leonard Lensink, Sjaak Smetsers, Marko C. J. D. van Eekelen	Machine Checked Formal Proof of a Scheduling Protocol for Smartcard Personalization.	FMICS	2007	DBLP DOI BibTeX RDF	simulation, verification, theorem proving, PVS, cyclic scheduling
21	Christian Engel 0002, Reiner Hähnle	Generating Unit Tests from Formal Proofs.	TAP	2007	DBLP DOI BibTeX RDF	theorem proving, program verification, model-based testing, unit testing, symbolic execution, test coverage, white-box testing
21	Achim D. Brucker, Burkhart Wolff	Test-Sequence Generation with Hol-TestGen with an Application to Firewall Testing.	TAP	2007	DBLP DOI BibTeX RDF	symbolic test case generations, theorem proving, computer security, black box testing, Isabelle/HOL, test sequence generation
21	Felicidad Aguado, José Luis Doncel, José María Molinelli, Gilberto Pérez 0001, Concepción Vidal, Ana María Vieites	Certified Genetic Algorithms: Crossover Operators for Permutations.	EUROCAST	2007	DBLP DOI BibTeX RDF	Calculus of Inductive Constructions, Genetic Algorithm, Specification, Theorem Proving, Crossover, Coq
21	Guillaume Burel, Claude Kirchner	Cut Elimination in Deduction Modulo by Abstract Completion.	LFCS	2007	DBLP DOI BibTeX RDF	Knuth-Bendix completion, automated deduction and interactive theorem proving, proof ordering, abstract canonical system, cut elimination, deduction modulo
21	Hongbo Li 0012	A recipe for symbolic geometric computing: long geometric product, BREEFS and Clifford factorization.	ISSAC	2007	DBLP DOI BibTeX RDF	null bracket algebra, symbolic geometric computing, geometric invariance, geometric theorem proving, conformal geometric algebra
21	Anatoli Degtyarev, Michael Fisher 0001, Boris Konev	Monodic temporal resolution.	ACM Trans. Comput. Log.	2006	DBLP DOI BibTeX RDF	Temporal logic, resolution, automated theorem proving
21	Lawrence C. Paulson	Defining functions on equivalence classes.	ACM Trans. Comput. Log.	2006	DBLP DOI BibTeX RDF	theorem proving, Equivalence classes, quotients
21	Jozef Hooman, Mark van der Zwaag	A semantics of communicating reactive objects with timing.	Int. J. Softw. Tools Technol. Transf.	2006	DBLP DOI BibTeX RDF	UML, Real-time, Formal methods, Theorem proving, Formal semantics
21	Chung-Hsien Wu, Jui-Feng Yeh, Yu-Sheng Lai	Semantic Segment Extraction and Matching for Internet FAQ Retrieval.	IEEE Trans. Knowl. Data Eng.	2006	DBLP DOI BibTeX RDF	deduction and theorem proving, Natural language processing, query formulation, retrieval models, knowledge processing
21	Nick C. Fiala, Keith M. Agre	Searching for Shortest Single Axioms for Groups of Exponent 6.	J. Autom. Reason.	2006	DBLP DOI BibTeX RDF	exponent, single axiom, group, automated theorem-proving
21	Oliver Pell	Verification of FPGA Layout Generators in Higher-Order Logic.	J. Autom. Reason.	2006	DBLP DOI BibTeX RDF	layout description, circuit verification, FPGA, theorem proving
21	Ruqian Lu, Daniel Dajun Zeng, Fei-Yue Wang 0001	AI Research in China: 50 Years down the Road.	IEEE Intell. Syst.	2006	DBLP DOI BibTeX RDF	AI in China, intelligence science, computer art and animation, knowware, geometrical theorem proving
21	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
21	Antonio Montes, Tomás Recio	Automatic Discovery of Geometry Theorems Using Minimal Canonical Comprehensive Gröbner Systems.	Automated Deduction in Geometry	2006	DBLP DOI BibTeX RDF	automatic discovering, comprehensive Gröbner system, canonical Gröbner system, automatic theorem proving
21	Erik Reeber, Jun Sawada	Combining ACL2 and an automated verification tool to verify a multiplier.	ACL2	2006	DBLP DOI BibTeX RDF	model checking, theorem proving, hardware verification
21	Warren A. Hunt Jr., Erik Reeber	A SAT-based procedure for verifying finite state machines in ACL2.	ACL2	2006	DBLP DOI BibTeX RDF	satisfiability solving, theorem proving, hardware verification, ACL2
21	Julien Schmaltz, Dominique Borrione	Towards a formal theory of on chip communications in the ACL2 logic.	ACL2	2006	DBLP DOI BibTeX RDF	formal theory, network on a chip, theorem proving, communication theory
21	David S. Hardin, Eric W. Smith, William D. Young	A robust machine code proof framework for highly secure applications.	ACL2	2006	DBLP DOI BibTeX RDF	cryptography, theorem proving, certification, symbolic simulation, ACL2, high-assurance, processor modeling
21	Constance L. Heitmeyer, Myla Archer, Elizabeth I. Leonard, John D. McLean	Formal specification and verification of data separation in a separation kernel for an embedded system.	CCS	2006	DBLP DOI BibTeX RDF	code verification, formal specification, theorem proving, formal model, separation kernel
21	Shoichi Morimoto, Shinjiro Shigematsu, Yuichi Goto, Jingde Cheng	A security specification verification technique based on the international standard ISO/IEC 15408.	SAC	2006	DBLP DOI BibTeX RDF	theorem-proving, Z notation, common criteria
21	Shuvendu K. Lahiri, Shaz Qadeer	Verifying properties of well-founded linked lists.	POPL	2006	DBLP DOI BibTeX RDF	first-order axiomatization, heap abstraction, well-founded linked lists, decision procedure, automated theorem proving
21	Ewen Denney, Bernd Fischer 0002	A generic annotation inference algorithm for the safety certification of automatically generated code.	GPCE	2006	DBLP DOI BibTeX RDF	hoare calculus, logical annotations, program verification, automated theorem proving, software certification, automated code generation
21	Christian Jacobi 0002, Christoph Berg	Formal Verification of the VAMP Floating Point Unit.	Formal Methods Syst. Des.	2005	DBLP DOI BibTeX RDF	IEEE standard 754, formal verification, theorem proving, PVS, floating point unit
21	Milos Besta, Frank A. Stomp	A Complete Mechanization of Correctness of a String-Preprocessing Algorithm.	Formal Methods Syst. Des.	2005	DBLP DOI BibTeX RDF	formal methods, pattern matching, theorem proving, PVS
21	Behzad Akbarpour, Sofiène Tahar, Abdelkader Dekdouk	Formalization of Fixed-Point Arithmetic in HOL.	Formal Methods Syst. Des.	2005	DBLP DOI BibTeX RDF	theorem-proving, floating-point arithmetic, fixed-point arithmetic, HOL
21	Jewgenij Botaschanjan, Leonid Kof, C. Kühnel, Maria Spichkova	Towards verified automotive software.	ACM SIGSOFT Softw. Eng. Notes	2005	DBLP DOI BibTeX RDF	verification, integration, theorem proving, automotive, time-triggered, model based software engineering
21	David Detlefs, Greg Nelson, James B. Saxe	Simplify: a theorem prover for program checking.	J. ACM	2005	DBLP DOI BibTeX RDF	Theorem proving, decision procedures, program checking
21	Bernard Jurkowiak, Chu Min Li, Gil Utard	A Parallelization Scheme Based on Work Stealing for a Class of SAT Solvers.	J. Autom. Reason.	2005	DBLP DOI BibTeX RDF	parallelism, automated theorem proving, SAT problem
21	M. Carmen Fernández Gago, Ullrich Hustadt, Clare Dixon, Michael Fisher 0001, Boris Konev	First-Order Temporal Verification in Practice.	J. Autom. Reason.	2005	DBLP DOI BibTeX RDF	temporal logics of knowledge, theorem proving, resolution, first-order temporal logic
21	Gilles Barthe, Pierre Courtieu, Guillaume Dufay, Simão Melo de Sousa	Tool-Assisted Specification and Verification of Typed Low-Level Languages.	J. Autom. Reason.	2005	DBLP DOI BibTeX RDF	virtual machine, theorem proving, Java Card, bytecode verification
21	Rohit Gheyi, Tiago Massoni	Formal refactorings for object models.	OOPSLA Companion	2005	DBLP DOI BibTeX RDF	theorem proving, object models, model refactoring
21	Bart Jacobs 0001, Wolter Pieters, Martijn Warnier	Statically checking confidentiality via dynamic labels.	WITS	2005	DBLP DOI BibTeX RDF	(Higher Order) theorem proving, formal verification, static analysis, abstract interpretation, confidentiality
21	Olha Shkaravska	Types with semantics: soundness proof assistant.	MERLIN	2005	DBLP DOI BibTeX RDF	type system, assertion, automated theorem proving, program logic
21	Kevin Donnelly, Hongwei Xi	Combining higher-order abstract syntax with first-order abstract syntax in ATS.	MERLIN	2005	DBLP DOI BibTeX RDF	ATS/LF, theorem proving, dependent types, higher-order abstract syntax, ATS
21	Yuki Chiba, Takahito Aoto 0001, Yoshihito Toyama	Program transformation by templates based on term rewriting.	PPDP	2005	DBLP DOI BibTeX RDF	inductive theorem proving, tree homomorphism, program transformation, term rewriting
21	Kazuhiro Ogata 0001, Kokichi Futatsugi	Equational Approach to Formal Analysis of TLS.	ICDCS	2005	DBLP DOI BibTeX RDF	security, verification, algebraic specification, rewriting, interactive theorem proving
21	Rohit Gheyi, Tiago Massoni, Paulo Borba	A rigorous approach for proving model refactorings.	ASE	2005	DBLP DOI BibTeX RDF	theorem proving, model refactoring
21	Jan Jürjens, Mark Yampolskiy	Code security analysis with assertions.	ASE	2005	DBLP DOI BibTeX RDF	code security analysis, cryto-based software, cryptographic protocols, first-order logic, assertions, automated theorem proving, C programs
21	Subash Shankar, Sinan Asa, Vladimir Sipos, Xiaowei Xu	Reasoning about real-time statecharts in the presence of semantic variations.	ASE	2005	DBLP DOI BibTeX RDF	model checking, semantics, temporal logics, theorem proving, statecharts
21	Gudmund Grov	Verifying the correctness of hume programs: an approach combining deductive and algorithmic reasoning.	ASE	2005	DBLP DOI BibTeX RDF	model checking, formal methods, formal verification, theorem proving, specification languages
21	Fatma Ozcan, V. S. Subrahmanian, Jürgen Dix	Improving Performance of Heterogeneous Agents.	Ann. Math. Artif. Intell.	2004	DBLP DOI BibTeX RDF	deduction and theorem proving, multi-agency, logical foundations, multi-agent reasoning, interoperability, distributed AI, heterogenous data sources
21	Toh Ne Win, Michael D. Ernst, Stephen J. Garland, Dilsun Kirli Kaynar, Nancy A. Lynch	Using simulated execution in verifying distributed algorithms.	Int. J. Softw. Tools Technol. Transf.	2004	DBLP DOI BibTeX RDF	Invariant detection, Static analysis, Theorem proving, Dynamic analysis
21	Christoph Walther, Stephan Schweitzer	Verification in the Classroom.	J. Autom. Reason.	2004	DBLP DOI BibTeX RDF	computer uses in education, deduction and automated theorem proving, computer-aided verification
21	Abhik Roychoudhury, K. Narayan Kumar, C. R. Ramakrishnan 0001, I. V. Ramakrishnan	An unfold/fold transformation framework for definite logic programs.	ACM Trans. Program. Lang. Syst.	2004	DBLP DOI BibTeX RDF	inductive theorem proving, Logic programming, program transformation, unfolding, folding
21	César A. Muñoz, Gilles Dowek, Victor Carreño	Modeling and verification of an air traffic concept of operations.	ISSTA	2004	DBLP DOI BibTeX RDF	air traffic management systems, model checking, theorem proving
21	Kazuhiro Ogata 0001, Kokichi Futatsugi	Equational Approach to Formal Verification of SET.	QSIC	2004	DBLP DOI BibTeX RDF	security, verification, algebraic specification, rewriting, interactive theorem proving, payment
21	Hongbo Li 0012	Symbolic computation in the homogeneous geometric model with clifford algebra.	ISSAC	2004	DBLP DOI BibTeX RDF	homogeneous model, automated theorem proving, symbolic computation, geometric algebra, clifford algebra
21	Marcelo Glusman, Shmuel Katz	A Mechanized Proof Environment for the Convenient Computations Proof Method.	Formal Methods Syst. Des.	2003	DBLP DOI BibTeX RDF	convenient computations, proof environment, deductive theorem proving, formal verification, PVS
21	John Harrison 0001	Formal Verification of Square Root Algorithms.	Formal Methods Syst. Des.	2003	DBLP DOI BibTeX RDF	formal verification, floating-point arithmetic, automated theorem proving
21	Susanne Graf	Preface by the section editor.	Int. J. Softw. Tools Technol. Transf.	2003	DBLP DOI BibTeX RDF	Goals: Conformance testing, Formal verification Techniques: Static analysis, Tool integration Application domains: Asynchronous systems, Performance evaluation, Model-checking, Markov chains, Theorem proving, Security protocols, Slicing, Partial-order reductions, Probabilistic systems, Component-based approaches
21	Louise A. Dennis, Graham Collins, Michael Norrish, Richard J. Boulton, Konrad Slind, Thomas F. Melham	The PROSPER toolkit.	Int. J. Softw. Tools Technol. Transf.	2003	DBLP DOI BibTeX RDF	Proof engine, Formal verification, Theorem proving, Tool integration
21	Jonathan Ford, Ian A. Mason	Formal Foundations of Operational Semantics.	High. Order Symb. Comput.	2003	DBLP DOI BibTeX RDF	contexts, theorem proving, operational semantics, PVS, calculus
21	Gerwin Klein, Martin Wildmoser	Verified Bytecode Subroutines.	J. Autom. Reason.	2003	DBLP DOI BibTeX RDF	Java, theorem proving, subroutines, dataflow analysis, Isabelle, bytecode verification
21	Jei-Wen Teng, Yih-Kuen Tsay	Composing Temporal-Logic Specifications with Machine Assistance.	FME	2003	DBLP DOI BibTeX RDF	Assumption-Guarantee, Compositional Specification, Formal Correctness, Temporal Logic, Theorem Proving, Concurrent Systems, PVS, Compositional Verification, Component-Based Software
21	Alberto Ciaffaglione, Luigi Liquori, Marino Miculan	Reasoning on an imperative object-based calculus in Higher Order Abstract Syntax.	MERLIN	2003	DBLP DOI BibTeX RDF	logical foundations of programming, object-based calculi with side-effects, program and system verification, logical frameworks, interactive theorem proving
21	Michael Norrish	Mechanising Hankin and Barendregt using the Gordon-Melham axioms.	MERLIN	2003	DBLP DOI BibTeX RDF	higher order abstract syntax, interactive theorem-proving
21	Yasuhiko Minamide, Koji Okuma	Verifying CPS transformations in Isabelle/HOL.	MERLIN	2003	DBLP DOI BibTeX RDF	program transformation, theorem proving, correctness proofs
21	Sanjit A. Seshia, Shuvendu K. Lahiri, Randal E. Bryant	A hybrid SAT-based decision procedure for separation logic with uninterpreted functions.	DAC	2003	DBLP DOI BibTeX RDF	theorem proving, decision procedures, boolean satisfiability, design verification
21	Karthikeyan Bhargavan, Davor Obradovic, Carl A. Gunter	Formal verification of standards for distance vector routing protocols.	J. ACM	2002	DBLP DOI BibTeX RDF	distance vector routing, network standards, model checking, Formal verification, routing protocols, AODV, SPIN, interactive theorem proving, HOL, RIP
21	Peter Frey, Radharamanan Radhakrishnan, Harold W. Carter, Philip A. Wilsey, Perry Alexander	A Formal Specification and Verification Framework for Time Warp-Based Parallel Simulation.	IEEE Trans. Software Eng.	2002	DBLP DOI BibTeX RDF	formal specification, formal verification, theorem proving, time warp, parallel discrete event simulation
21	Jon Whittle 0001, Alan Bundy, Richard J. Boulton	Proofs-as-Programs as a Framework for the Design of an Analogy-Based ML Editor.	Formal Aspects Comput.	2002	DBLP DOI BibTeX RDF	Programming environments, Functional programming, Theorem proving
21	J Strother Moore, George Porter	The apprentice challenge.	ACM Trans. Program. Lang. Syst.	2002	DBLP DOI BibTeX RDF	Java, theorem proving, Java Virtual Machine, mutual exclusion, operational semantics, parallel and distributed computation
21	Jozef Hooman, Jaco van de Pol	Formal verification of replication on a distributed data space architecture.	SAC	2002	DBLP DOI BibTeX RDF	data space architecture, model-checking, formal verification, coordination, theorem proving
21	J Strother Moore	Functional formal methods.	ICFP	2002	DBLP DOI BibTeX RDF	functional programming, Java Virtual Machine, microarchitecture, software verification, Common Lisp, hardware verification, mechanical theorem proving
21	Steven Shapiro, Yves Lespérance, Hector J. Levesque	The cognitive agents specification language and verification environment for multiagent systems.	AAMAS	2002	DBLP DOI BibTeX RDF	agent specification languages, theorem proving, proof assistants, verification tools
21	Michael Fisher 0001, Clare Dixon, Martin Peim	Clausal temporal resolution.	ACM Trans. Comput. Log.	2001	DBLP DOI BibTeX RDF	temporal logic, theorem proving, resolution
21	Raymond Reiter	On knowledge-based programming with sensing in the situation calculus.	ACM Trans. Comput. Log.	2001	DBLP DOI BibTeX RDF	dynamic closed-world assumption, sensing and knowledge, situation calculus programming languages, theorem-proving, situation calculus
21	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
21	Maria Luisa Bonet, Nicola Galesi	Optimality of size-width tradeoffs for resolution.	Comput. Complex.	2001	DBLP DOI BibTeX RDF	complexity of proofs, automated theorem proving.¶ Subject classification. 03F20, 03B05, Resolution, 68T15
21	Jörg H. Siekmann, Graham Wrightson	Erratum: a counterexample to W. Bibel's and E. Eder's strong completeness result for connection graph resolution.	J. ACM	2001	DBLP DOI BibTeX RDF	computational logic, mechanical theorem proving, mathematical logic
21	David A. Basin, Harald Ganzinger	Automated complexity analysis based on ordered resolution.	J. ACM	2001	DBLP DOI BibTeX RDF	ordered resolution, automated theorem proving, complexity analysis, first-order theories
21	Angelo Gargantini, Angelo Morzenti	Automated deductive requirements analysis of critical systems.	ACM Trans. Softw. Eng. Methodol.	2001	DBLP DOI BibTeX RDF	finite variability, temporal logic, theorem proving, hybrid systems, state-transition systems
21	Oscar Slotosch	Modelling and Validation: AUTOFOCUS and Quest.	Formal Aspects Comput.	2000	DBLP DOI BibTeX RDF	Model checking, Interactive theorem proving, State transition diagrams, Event traces
21	Andrew P. Martin	Relating Z and First-Order Logic.	Formal Aspects Comput.	2000	DBLP DOI BibTeX RDF	Undefinedness, Models, Tools, Theorem proving, Logics, Schemas, Z notation
21	Padmanabhan Krishnan	Consistency checks for UML.	APSEC	2000	DBLP DOI BibTeX RDF	UML consistency checking, state predicates, PVS theorem prover, Prototype Verification System, partially specified systems, behavioural description, Unified Modeling Language, formal verification, theorem proving, specification languages, diagrams, computation history, UML diagrams, dynamic aspects
21	Cynthia Dwork, Moni Naor	Zaps and Their Applications.	FOCS	2000	DBLP DOI BibTeX RDF	zap, witness-indistinguishable protocol, shared random string model, verifiable pseudo-random bit generators, concurrent deniable authentication, computational complexity, cryptography, NP completeness, theorem proving, public keys, zero-knowledge proofs, verifier, concurrent zero knowledge
21	Richard Cleve, John Watrous	Fast parallel circuits for the quantum Fourier transform.	FOCS	2000	DBLP DOI BibTeX RDF	fast parallel circuits, quantum Fourier transform, QFT, circuit depth, constant error, depth bound, polynomial size, classical polynomial-time processing, depth complexity, arbitrary modulus, lower bound, theorem proving, quantum computing, Fourier transforms, upper bound, circuit complexity, circuit complexity, quantum circuits, factoring algorithm
21	Jeff Kahn 0001, Jeong Han Kim, László Lovász 0001, Van H. Vu	The Cover Time, the Blanket Time, and the Matthews Bound.	FOCS	2000	DBLP DOI BibTeX RDF	blanket time, Matthews bound, Matthews bounds, deterministic-polynomial time algorithm, computational complexity, approximation algorithm, graph theory, graph, theorem proving, random walk, deterministic algorithms, approximation theory, stationary distribution, cover time
21	Russell A. Martin, Dana Randall	Sampling Adsorbing Staircase Walks Using a New Markov Chain Decomposition Method.	FOCS	2000	DBLP DOI BibTeX RDF	adsorbing staircase walks, Markov chain decomposition method, lattice paths, diagonal steps, local Markov chain, /spl lambda//sup /spl kappa//, Gibbs measure, first proof, statistical physics community, Markov chain, theorem proving, Markov processes, lambda calculus, state space, decomposition technique
21	John Watrous	Succinct quantum proofs for properties of finite groups.	FOCS	2000	DBLP DOI BibTeX RDF	succinct quantum proofs, finite group properties, quantum computational variant, quantum proof, quantum state, NP-type proof, black-box groups, group operations, group oracle, Group Non-Membership problem, bounded error, simple proof, quantum proofs, classical proofs, group properties, computational complexity, theorem proving, quantum computing, quantum computer, certificate, nondeterminism, polynomial time, strings, group theory, finite groups
21	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
21	Daniel Brand	A Software Falsifier.	ISSRE	2000	DBLP DOI BibTeX RDF	static analysis, theorem proving, data-flow analysis, symbolic execution