The FacetedDBLP logo    Search for: in:

Disable automatic phrases ?     Syntactic query expansion: ?

Searching for phrase theorem prover (changed automatically) with no syntactic query expansion in all metadata.

Publication years (Num. hits)
1970-1977 (15) 1978-1984 (22) 1985-1986 (20) 1987-1988 (36) 1989 (25) 1990 (26) 1991 (18) 1992 (45) 1993 (34) 1994 (32) 1995 (27) 1996 (43) 1997 (37) 1998 (59) 1999 (52) 2000 (62) 2001 (54) 2002 (65) 2003 (57) 2004 (82) 2005 (78) 2006 (83) 2007 (75) 2008 (68) 2009 (59) 2010 (19) 2011 (23) 2012-2013 (26) 2014 (18) 2015 (22) 2016-2017 (29) 2018 (21) 2019-2020 (31) 2021 (15) 2022 (23)
Publication types (Num. hits)
article(237) book(1) incollection(1) inproceedings(1147) phdthesis(6) proceedings(9)
Venues (Conferences, Journals, ...)
CADE(154) ACL2(108) TPHOLs(80) CAV(43) J. Autom. Reason.(42) IJCAR(32) CoRR(25) LPAR(22) TABLEAUX(22) Formal Aspects Comput.(18) FME(16) TYPES(16) FMCAD(15) SEFM(14) POPL(13) TACAS(13) More (+10 of total 396)
GrowBag graphs for keyword ? (Num. hits/coverage)

Group by:
The graphs summarize 1057 occurrences of 524 keywords

Results
Found 1401 publication records. Showing 1401 according to the selection in the facets
Hits ? Authors Title Venue Year Link Author keywords
75Dipankar Sarkar 0001, S. C. De Sarkar A Theorem Prover for Verifying Iterative Programs Over Integers. Search on Bibsonomy IEEE Trans. Software Eng. The full citation details ... 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
72Raul H. C. Lopes, Mark Tarver Inducing Theorem Provers from Proofs. Search on Bibsonomy ICTAI The full citation details ... 1997 DBLP  DOI  BibTeX  RDF theorem prover induction, automatic theorem prover generation, proof examples, intuitionistic propositional calculus, depth-first search strategy, loop detection, inductive generalization, machine learning, theorem proving
70George C. Necula, Peter Lee 0001 Proof Generation in the Touchstone Theorem Prover. Search on Bibsonomy CADE The full citation details ... 2000 DBLP  DOI  BibTeX  RDF
68Stefan Gerberding DT - An Automated Theorem Prover for Multiple-Valued First-Order Predicate Logics. Search on Bibsonomy ISMVL The full citation details ... 1996 DBLP  DOI  BibTeX  RDF Deep Thought, multiple-valued first-order logics, lemma generation, tableau expansion, branch closure, theorem proving, multivalued logic, multiple-valued logics, quantifiers, first-order predicate logic, truth tables, automated theorem prover
66Boutheina Chetali Formal Verification of Concurrent Programs Using the Larch Prover. Search on Bibsonomy IEEE Trans. Software Eng. The full citation details ... 1998 DBLP  DOI  BibTeX  RDF theorem prover methodology, Larch prover, computer-checked proof, Formal verification, communication protocol, protocol verification, UNITY
66Yoshinao Isobe, Markus Roggenbach A Generic Theorem Prover of CSP Refinement. Search on Bibsonomy TACAS The full citation details ... 2005 DBLP  DOI  BibTeX  RDF
64Anand Chavan, Shiu-Kai Chin, Shahid Ikram, Jang Dae Kim, Juin-Yeu Zu Extending VLSI design with higher-order logic. Search on Bibsonomy ICCD The full citation details ... 1995 DBLP  DOI  BibTeX  RDF Cambridge Higher-Order Logic theorem-prover, microprogram sequencer, Am2910, VLSI, formal verification, formal verification, logic testing, theorem proving, logic design, logic CAD, VLSI design, higher-order logic, theorem-prover, design environment, instruction-set architecture, VLSI CAD
62Robert S. Boyer, J. Strother Moore A Theorem Prover for a Computational Logic. Search on Bibsonomy CADE The full citation details ... 1990 DBLP  DOI  BibTeX  RDF
59Viktor K. Sabelfeld, Kai Kapp Numeric Types in Formal Synthesis. Search on Bibsonomy Ershov Memorial Conference The full citation details ... 2003 DBLP  DOI  BibTeX  RDF correct hardware synthesis, formal specification, higher-order logic, theorem prover, arithmetic operations
58Kenneth Roe The Heuristic Theorem Prover: Yet Another SMT Modulo Theorem Prover. Search on Bibsonomy CAV The full citation details ... 2006 DBLP  DOI  BibTeX  RDF
58Maarten de Mol, Marko C. J. D. van Eekelen A Proof Tool Dedicated to Clean - The First Prototype. Search on Bibsonomy AGTIVE The full citation details ... 1999 DBLP  DOI  BibTeX  RDF
56Sa'ed Abed, Otmane Aït Mohamed, Ghiath Al Sammane Reachability analysis using multiway decision graphs in the HOL theorem prover. Search on Bibsonomy SAC The full citation details ... 2008 DBLP  DOI  BibTeX  RDF reachability analysis, HOL, multiway decision graphs
56Jun Sawada, Erik Reeber ACL2SIX: A Hint used to Integrate a Theorem Prover and an Automated Verification Tool. Search on Bibsonomy FMCAD The full citation details ... 2006 DBLP  DOI  BibTeX  RDF
56Blayne E. Mayfield, Timothy B. Baird STP: A Simple Theorem Prover for IBM-PC Compatible Computers. Search on Bibsonomy SIGSMALL/PC Symposium The full citation details ... 1990 DBLP  DOI  BibTeX  RDF IBM PC, Turbo Pascal
55Rajeev Goré, Joachim Posegga, Andrew Slater, Harald Vogt System Description: card TAP: The First Theorem Prover on a Smart Card. Search on Bibsonomy CADE The full citation details ... 1998 DBLP  DOI  BibTeX  RDF
55Jieh Hsiang, Mandayam K. Srivas PROLOG-Based Inductive Theorem Proving. Search on Bibsonomy FSTTCS The full citation details ... 1985 DBLP  DOI  BibTeX  RDF
53David S. Hardin, Matthew Wilding, David A. Greve Transforming the Theorem Prover into a Digital Design Tool: From Concept Car to Off-Road Vehicle. Search on Bibsonomy CAV The full citation details ... 1998 DBLP  DOI  BibTeX  RDF
52Kun Wei, James Heather Embedding the Stable Failures Model of CSP in PVS. Search on Bibsonomy IFM The full citation details ... 2005 DBLP  DOI  BibTeX  RDF CSP, deadlock, determinism, liveness, theorem prover
52Boutheina Chetali, Barbara Heyd Formal Verification of Concurrent Programs in LP and in COQ: A Comparative Analysis. Search on Bibsonomy TPHOLs The full citation details ... 1997 DBLP  DOI  BibTeX  RDF theorem prover methodology, Larch Prover, Computer Checked Proof, Formal Verification, Unity, Coq
52Joseph P. Near, William E. Byrd, Daniel P. Friedman alpha-leanTAP: A Declarative Theorem Prover for First-Order Classical Logic. Search on Bibsonomy ICLP The full citation details ... 2008 DBLP  DOI  BibTeX  RDF
52Abdessamad Imine, Michaël Rusinowitch Applying a Theorem Prover to the Verification of Optimistic Replication Algorithms. Search on Bibsonomy Rewriting, Computation and Proof The full citation details ... 2007 DBLP  DOI  BibTeX  RDF
50Sa'ed Abed, Otmane Aït Mohamed MDGs Reduction Technique Based on the HOL Theorem Prover. Search on Bibsonomy ISMVL The full citation details ... 2010 DBLP  DOI  BibTeX  RDF Soundness, Reduction Techniques, Multiway Decision Graphs, HOL Theorem Prover
50Ian Horrocks 0001, Andrei Voronkov Reasoning Support for Expressive Ontology Languages Using a Theorem Prover. Search on Bibsonomy FoIKS The full citation details ... 2006 DBLP  DOI  BibTeX  RDF
49Ryuzo Hasegawa, Miyuki Koshimura, Hiroshi Fujita 0002 MGTP: A Parallel Theorem Prover Based on Lazy Model Generation. Search on Bibsonomy CADE The full citation details ... 1992 DBLP  DOI  BibTeX  RDF
49Mark Tarver An Examination of the Prolog Technology Theorem-Prover. Search on Bibsonomy CADE The full citation details ... 1990 DBLP  DOI  BibTeX  RDF PTTP, metalevel reasoning, Prolog Normal Form, refinement
48Marcel Oliveira, Ana Cavalcanti 0001, Jim Woodcock Unifying Theories in ProofPower-Z. Search on Bibsonomy UTP The full citation details ... 2006 DBLP  DOI  BibTeX  RDF Unifying Theories of Programming, theorem prover
48Mizuhito Ogawa, Eiichi Horita, Satoshi Ono Proving Properties of Incremental Merkle Trees. Search on Bibsonomy CADE The full citation details ... 2005 DBLP  DOI  BibTeX  RDF temporal authentication, theorem prover, Merkle tree
48Virginie Thion, Serenella Cerrito, Marta Cialdea Mayer A General Theorem Prover for Quantified Modal Logics. Search on Bibsonomy TABLEAUX The full citation details ... 2002 DBLP  DOI  BibTeX  RDF
48Tanel Tammet A Resolution Theorem Prover for Intuitonistic Logic. Search on Bibsonomy CADE The full citation details ... 1996 DBLP  DOI  BibTeX  RDF
47Mihir Parang Mehta Formalising Filesystems in the ACL2 Theorem Prover: an Application to FAT32. Search on Bibsonomy ACL2 The full citation details ... 2018 DBLP  DOI  BibTeX  RDF
47Gernot Stenz, Andreas Wolf 0005 Scheduling Methods for Parallel Automated Theorem Proving. Search on Bibsonomy Canadian Conference on AI The full citation details ... 2000 DBLP  DOI  BibTeX  RDF
45Randall W. Lichota, Grace L. Hammonds, Stephen H. Brackin Verifying The Correctness Of Cryptographic Protocols Using "Convince". Search on Bibsonomy ACSAC The full citation details ... 1996 DBLP  DOI  BibTeX  RDF Convince, theorem proving component, commercial computer aided software engineering tool, StP/OMT, textual notations, Higher Order Logic theorem prover, protocols, cryptographic protocols, authentication protocols, front-end, belief logic, correctness verification, automated support
45Dru McCandless, Leo Obrst, Shayn Hawthorne Dynamic Web Service Assembly Using OWL and a Theorem Prover. Search on Bibsonomy ICSC The full citation details ... 2009 DBLP  DOI  BibTeX  RDF
45Aaron Richard Coble Formalized Information-Theoretic Proofs of Privacy Using the HOL4 Theorem-Prover. Search on Bibsonomy Privacy Enhancing Technologies The full citation details ... 2008 DBLP  DOI  BibTeX  RDF
45Shinya Umeno, Nancy A. Lynch Proving Safety Properties of an Aircraft Landing Protocol Using I/O Automata and the PVS Theorem Prover: A Case Study. Search on Bibsonomy FM The full citation details ... 2006 DBLP  DOI  BibTeX  RDF
45Tadashi Takahashi, Hidetsune Kobayashi The Effect of the Theorem Prover in Cognitive Science. Search on Bibsonomy International Conference on Computational Science (1) The full citation details ... 2006 DBLP  DOI  BibTeX  RDF
45Nicola Olivetti, Gian Luca Pozzato CondLean: A Theorem Prover for Conditional Logics. Search on Bibsonomy TABLEAUX The full citation details ... 2003 DBLP  DOI  BibTeX  RDF
45Jens Happe The MODPROF Theorem Prover. Search on Bibsonomy IJCAR The full citation details ... 2001 DBLP  DOI  BibTeX  RDF
45David Spelt, Susan Even A Theorem Prover-Based Analysis Tool for Object-Oriented Databases. Search on Bibsonomy TACAS The full citation details ... 1999 DBLP  DOI  BibTeX  RDF
45Aline Deruyver EMMY: A Refutational Theorem Prover for First-Order Logic with Equation. Search on Bibsonomy RTA The full citation details ... 1991 DBLP  DOI  BibTeX  RDF
45Johann Schumann, Reinhold Letz PARTHEO: A High-Performance Parallel Theorem Prover. Search on Bibsonomy CADE The full citation details ... 1990 DBLP  DOI  BibTeX  RDF Warren Abstract Machine, message passing, Theorem proving, first-order logic, transputers, or-parallelism, model elimination, connection method
45Heikki Tuominen Proving Properties of Elementary Net Systems with a Special-Purpose Theorem Prover. Search on Bibsonomy Automatic Verification Methods for Finite State Systems The full citation details ... 1989 DBLP  DOI  BibTeX  RDF
45Mark E. Stickel A prolog Technology Theorem Prover: Implementation by an Extended Prolog Compiler. Search on Bibsonomy CADE The full citation details ... 1986 DBLP  DOI  BibTeX  RDF
45Paul Y. Gloess An Experiment with the Boyer-Moore Theorem Prover: A Proof of the Correctness of a Simple Parser of Expressions. Search on Bibsonomy CADE The full citation details ... 1980 DBLP  DOI  BibTeX  RDF
45Johann Schumann, Bernd Fischer 0002 NORA/HAMMR: Making Deduction-Based Software Component Retrieval Practical. Search on Bibsonomy ASE The full citation details ... 1997 DBLP  DOI  BibTeX  RDF deduction-based software component retrieval, NORA/HAMMR, search keys, proof tasks, rejection filters, model checking techniques, confirmation filter, software reusability, signature matching, automated theorem prover
43John Matthews, J Strother Moore, Sandip Ray, Daron Vroon 0001 Verification Condition Generation Via Theorem Proving. Search on Bibsonomy LPAR The full citation details ... 2006 DBLP  DOI  BibTeX  RDF
43Michael Barnett 0001, K. Rustan M. Leino Weakest-precondition of unstructured programs. Search on Bibsonomy PASTE The full citation details ... 2005 DBLP  DOI  BibTeX  RDF
43Deepak Kapur, Mahadevan Subramaniam Using an induction prover for verifying arithmetic circuits. Search on Bibsonomy Int. J. Softw. Tools Technol. Transf. The full citation details ... 2000 DBLP  DOI  BibTeX  RDF Induction, Automated reasoning, Decision procedures, Rewriting, Arithmetic circuits, Hardware verification
43Dennis de Champeaux Subproblem finder and instance checker, two cooperating modules for theorem provers. Search on Bibsonomy J. ACM The full citation details ... 1986 DBLP  DOI  BibTeX  RDF
42Xia Wu, Jigui Sun, Kun Hou An Extension Rule Based First-Order Theorem Prover. Search on Bibsonomy KSEM The full citation details ... 2006 DBLP  DOI  BibTeX  RDF
42Christoph Benzmüller, Volker Sorge, Mateja Jamnik, Manfred Kerber Can a Higher-Order and a First-Order Theorem Prover Cooperate?. Search on Bibsonomy LPAR The full citation details ... 2004 DBLP  DOI  BibTeX  RDF
42Koji Iwanuma Lemma Matching for a PTTP-based Top-down Theorem Prover. Search on Bibsonomy CADE The full citation details ... 1997 DBLP  DOI  BibTeX  RDF
42Hans Jürgen Ohlbach, Graham Wrightson Solving a Problem in Relevance Logic with an Automated Theorem Prover. Search on Bibsonomy CADE The full citation details ... 1984 DBLP  DOI  BibTeX  RDF
42Osman Hasan, Sofiène Tahar Performance Analysis and Functional Verification of the Stop-and-Wait Protocol in HOL. Search on Bibsonomy J. Autom. Reason. The full citation details ... 2009 DBLP  DOI  BibTeX  RDF Real-time systems, Communication protocols, Higher-order-logic, Probability theory, HOL theorem prover
42Greta Yorsh, Thomas Ball, Mooly Sagiv Testing, abstraction, theorem proving: better together! Search on Bibsonomy ISSTA The full citation details ... 2006 DBLP  DOI  BibTeX  RDF fabricated states, state-based coverage, testing, abstraction, program analysis, abstract interpretation, coverage, theorem prover, software fault injection, adequacy criteria
42Wendy MacCaull Finite Algebraic Models for Residuated Logic. Search on Bibsonomy ISMVL The full citation details ... 1995 DBLP  DOI  BibTeX  RDF finite algebraic models, residuated logic, model pruning, nonclassical logics, combinatorial explosions, structure theorems, residuated algebras, theorem proving, inference mechanisms, search problems, multivalued logic, approximate reasoning, substructural logics, algebraic semantics, automated theorem prover
42David R. Lester, Sava Mintchev Towards Machine-Checked Compiler Correctness for Higher-order Pure Functional Languages. Search on Bibsonomy CSL The full citation details ... 1994 DBLP  DOI  BibTeX  RDF Congruence Proof, Lambda Calculus, Denotational Semantics, Theorem Prover, Compiler Correctness
41André Platzer, Jan-David Quesel KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description). Search on Bibsonomy IJCAR The full citation details ... 2008 DBLP  DOI  BibTeX  RDF verification of hybrid systems, decision procedures, computer algebra, automated theorem proving, dynamic logic
41Richard Bonichon, David Delahaye, Damien Doligez Zenon : An Extensible Automated Theorem Prover Producing Checkable Proofs. Search on Bibsonomy LPAR The full citation details ... 2007 DBLP  DOI  BibTeX  RDF
41Kaustuv Chaudhuri, Frank Pfenning A Focusing Inverse Method Theorem Prover for First-Order Linear Logic. Search on Bibsonomy CADE The full citation details ... 2005 DBLP  DOI  BibTeX  RDF
41Kenneth L. McMillan An Interpolating Theorem Prover. Search on Bibsonomy TACAS The full citation details ... 2004 DBLP  DOI  BibTeX  RDF
41Joshua S. Hodas, Naoyuki Tamura lolliCop - A Linear Logic Implementation of a Lean Connection-Method Theorem Prover for First-Order Classical Logic. Search on Bibsonomy IJCAR The full citation details ... 2001 DBLP  DOI  BibTeX  RDF
41Yves Ledru Identifying Pre-Conditions with the Z/EVES Theorem Prover. Search on Bibsonomy ASE The full citation details ... 1998 DBLP  DOI  BibTeX  RDF
41Maria Paola Bonacina The Clause-Diffusion Theorem Prover Peers-mcd (System Description). Search on Bibsonomy CADE The full citation details ... 1997 DBLP  DOI  BibTeX  RDF
41Scott Hazelhurst, Carl-Johan H. Seger A simple theorem prover based on symbolic trajectory evaluation and BDD's. Search on Bibsonomy IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. The full citation details ... 1995 DBLP  DOI  BibTeX  RDF
39Jens Otten leanCoP 2.0and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions). Search on Bibsonomy IJCAR The full citation details ... 2008 DBLP  DOI  BibTeX  RDF
39Mario Carneiro Metamath Zero: Designing a Theorem Prover Prover. Search on Bibsonomy CICM The full citation details ... 2020 DBLP  DOI  BibTeX  RDF
39Shuling Wang, Naijun Zhan, Liang Zou An Improved HHL Prover: An Interactive Theorem Prover for Hybrid Systems. Search on Bibsonomy ICFEM The full citation details ... 2015 DBLP  DOI  BibTeX  RDF
39Aleksandar Krapez, Miodrag Kapetanovic, Zoran Ognjanovic, Tatjana Petrovic Prover 91 - A Parallel Theorem Prover (Extended Abstract). Search on Bibsonomy TABLEAUX The full citation details ... 1992 DBLP  BibTeX  RDF
39Steven Greenbaum, David A. Plaisted The Illinois Prover: A General Purpose Resolution Theorem Prover. Search on Bibsonomy CADE The full citation details ... 1986 DBLP  DOI  BibTeX  RDF
39Shang-Ching Chou GEO-Prover - A Geometry Theorem Prover Developed at UT. Search on Bibsonomy CADE The full citation details ... 1986 DBLP  DOI  BibTeX  RDF
38Adolfo Gustavo Serra Seca Neto, Marcelo Finger Effective Prover for Minimal Inconsistency Logic. Search on Bibsonomy IFIP AI The full citation details ... 2006 DBLP  DOI  BibTeX  RDF
38Christoph Benzmüller, Lawrence C. Paulson, Frank Theiss, Arnaud Fietzke LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description). Search on Bibsonomy IJCAR The full citation details ... 2008 DBLP  DOI  BibTeX  RDF
38Dale Vaillancourt, Rex L. Page, Matthias Felleisen ACL2 in DrScheme. Search on Bibsonomy ACL2 The full citation details ... 2006 DBLP  DOI  BibTeX  RDF DrScheme, TeachScheme!, formal methods, pedagogy, ACL2
38Noboru Matsuda, Kurt VanLehn GRAMY: A Geometry Theorem Prover Capable of Construction. Search on Bibsonomy J. Autom. Reason. The full citation details ... 2004 DBLP  DOI  BibTeX  RDF automated geometry theorem proving, search control, intelligent tutoring system, constraint satisfaction problem, construction
38Hasan Amjad Programming a Symbolic Model Checker in a Fully Expansive Theorem Prover. Search on Bibsonomy TPHOLs The full citation details ... 2003 DBLP  DOI  BibTeX  RDF
38Gernot Stenz, Andreas Wolf 0005 E-SETHEO: Design, Configuration and Use of a Parallel Automated Theorem Prover. Search on Bibsonomy Australian Joint Conference on Artificial Intelligence The full citation details ... 1999 DBLP  DOI  BibTeX  RDF
38Deepak Kapur, Mahadevan Subramaniam Mechanizing Reasoning about Large Finite Tables in a Rewrite Based Theorem Prover. Search on Bibsonomy ASIAN The full citation details ... 1998 DBLP  DOI  BibTeX  RDF
38Sten Agerholm, Jacob Frost An Isabelle-Based Theorem Prover for VDM-SL. Search on Bibsonomy TPHOLs The full citation details ... 1997 DBLP  DOI  BibTeX  RDF
38Jeffrey J. Joyce, Carl-Johan H. Seger The HOL-Voss System: Model-Checking inside a General-Purpose Theorem-Prover. Search on Bibsonomy HUG The full citation details ... 1993 DBLP  DOI  BibTeX  RDF
38Mark E. Stickel A Prolog Technology Theorem Prover: A New Exposition and Implementation in Prolog. Search on Bibsonomy DISCO The full citation details ... 1990 DBLP  DOI  BibTeX  RDF
38Sa'ed Abed, Otmane Aït Mohamed, Ghiath Al Sammane An Abstract Reachability Approach by Combining HOL Induction and Multiway Decision Graphs. Search on Bibsonomy J. Comput. Sci. Technol. The full citation details ... 2009 DBLP  DOI  BibTeX  RDF correctness, reachability analysis, multiway decision graphs, HOL theorem prover
38Osman Hasan, Sofiène Tahar Using Theorem Proving to Verify Expectation and Variance for Discrete Random Variables. Search on Bibsonomy J. Autom. Reason. The full citation details ... 2008 DBLP  DOI  BibTeX  RDF Coupon collector’s problem, Probabilistic analysis, Higher-order-logic, Probability theory, Statistical properties, HOL theorem prover
38Julien Narboux A Graphical User Interface for Formal Proofs in Geometry. Search on Bibsonomy J. Autom. Reason. The full citation details ... 2007 DBLP  DOI  BibTeX  RDF Interface, Geometry, Automated theorem proving, Theorem prover, Proof assistant, Coq, Dynamic geometry
38Padmanabhan Krishnan Consistency checks for UML. Search on Bibsonomy APSEC The full citation details ... 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
38Keith Vanderveen, C. V. Ramamoorthy Partial instantiation theorem proving for distributed resource location. Search on Bibsonomy COMPSAC The full citation details ... 1997 DBLP  DOI  BibTeX  RDF partial instantiation theorem prover, distributed resource location, INSTANT, clausal form, non clausal form, GSAT algorithm, propositional sentence, request matching, CORBA Object Trading Service, KIF, theorem proving, satisfiability, first order logic, KQML
38Dieter Fensel, Arno Schönegge Using KIV to Specify and Verify Architectures of Knowledge-Based Systems. Search on Bibsonomy ASE The full citation details ... 1997 DBLP  DOI  BibTeX  RDF reusable elements, Karlsruhe interactive verifier, algorithmic specification, interactive theorem prover, proof management, proof reuse, formal specification, formal specifications, knowledge-based systems, specification language, abstract data types, dynamic logic, functional specification
38Savi Maharaj, Juan Bicarregui On the Verification of VDM Specification and Refinement with PVS. Search on Bibsonomy ASE The full citation details ... 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
38Yves Ledru Using KIDS as a Tool Support for VDM. Search on Bibsonomy ICSE The full citation details ... 1996 DBLP  BibTeX  RDF KIDS, REGROUP, VDM specifications, correctness preserving transformations, executable prototypes synthesis, proof of consistency, formal specification, REFINE, theorem proving, program verification, specification languages, tool support, theorem prover, VDM
38Pierre Bieber Formal Techniques for an ITSEC-E4 Secure Gateway. Search on Bibsonomy ACSAC The full citation details ... 1996 DBLP  DOI  BibTeX  RDF ITSEC-E4 secure gateway, interactive theorem prover, Information Technology Security Evaluation Criteria, formal specification, security policy, security architecture, formal technique, functional specifications
38David Cyrluk, Mandayam K. Srivas Theorem proving: not an esoteric diversion, but the unifying framework for industrial verification. Search on Bibsonomy ICCD The full citation details ... 1995 DBLP  DOI  BibTeX  RDF industrial hardware verification, industrial verification, formal verification, logic testing, theorem proving, theorem prover, hardware verification
38Ramayya Kumar, Thomas Kropf, Klaus Schneider 0001 Formal synthesis of circuits with a simple handshake protocol. Search on Bibsonomy VLSI Design The full citation details ... 1995 DBLP  DOI  BibTeX  RDF formal circuit synthesis, preproven building blocks, higher-order temporal operators, parametrized data signals, sequentially composed modules, parallel module composition, protocols, high level synthesis, logic design, operator semantics, template, formal logic, correctness proofs, synchronous circuits, handshake protocol, HOL theorem prover
38Milica Barjaktarovic, Shiu-Kai Chin, Kamal Jabbour Formal specification and verification of communication protocols using automated tools . Search on Bibsonomy ICECCS The full citation details ... 1995 DBLP  DOI  BibTeX  RDF OSI protocol, large models, simulation, modelling, formal specification, formal specification, testing, protocols, formal verification, software tools, validation, theorem proving, process algebra, communication protocols, open systems, algebra, formal logic, automated tools, model checker, model testing, complex models, automated theorem prover
38Robert S. Boyer, Yuan Yu Automated Correctness Proofs of Machine Code Programs for a Commercial Microprocessor. Search on Bibsonomy CADE The full citation details ... 1992 DBLP  DOI  BibTeX  RDF Nqthm, Boyer-Moore Theorem Prover, Gnu, Ada, C, Automated reasoning, object code, formal program verification
38Gerald M. Karam, Raymond J. A. Buhr Temporal Logic-Based Deadlock Analysis For Ada. Search on Bibsonomy IEEE Trans. Software Eng. The full citation details ... 1991 DBLP  DOI  BibTeX  RDF temporal logic-based specification language, deadlock analyzer, Timebench, concurrent system-design environment, COL, linear-time temporal logic, formal basis, axiomatic reasoning, deadlock analysis tool, reasoning power, Ada designs, systemwide deadlock-free, deadlock algorithm, finite systems, worst-case computational complexity, gas station, layered communications system, computational complexity, Ada, logic programming, temporal logic, Prolog, specification language, specification languages, inference mechanisms, system recovery, theorem prover, readers, dining philosophers, writers
38William R. Bevier, Jørgen F. Søgaard-Andersen Mechanically Checked Proofs of Kernel Specification. Search on Bibsonomy CAV The full citation details ... 1991 DBLP  DOI  BibTeX  RDF mechanical proof checking, Boyer-Moore Theorem Prover, Kernel, labeled transition systems, safety properties, stepwise development
38Albert John Camilleri Mechanizing CSP Trace Theory in Higher Order Logic. Search on Bibsonomy IEEE Trans. Software Eng. The full citation details ... 1990 DBLP  DOI  BibTeX  RDF mechanising CSP trace theory, general-purpose theorem prover, formal specification, theorem proving, formal logic, higher order logic, communicating sequential processes
38Dipankar Sarkar 0001, S. C. De Sarkar Some Inference Rules for Integer Arithmetic for Verification of Flowchart Programs on Integers. Search on Bibsonomy IEEE Trans. Software Eng. The full citation details ... 1989 DBLP  DOI  BibTeX  RDF flowchart programs, first-order rules, algebraic expressions, proof construction process, human thought process, user provided axioms, verification, theorem proving, program verification, inference mechanisms, inference rules, theorem prover, integer arithmetic
38William R. Bevier Kit: A Study in Operating System Verification. Search on Bibsonomy IEEE Trans. Software Eng. The full citation details ... 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
37Weiqiang Kong, Takahiro Seino, Kokichi Futatsugi, Kazuhiro Ogata 0001 A Lightweight Integration of Theorem Proving and Model Checking for System Verification. Search on Bibsonomy APSEC The full citation details ... 2005 DBLP  DOI  BibTeX  RDF
Displaying result #1 - #100 of 1401 (100 per page; Change: )
Pages: [1][2][3][4][5][6][7][8][9][10][>>]
Valid XHTML 1.1! Valid CSS! [Valid RSS]
Maintained by Jörg Diederich.
Based upon DBLP by Michael Ley.
open data data released under the ODC-BY 1.0 license