|
|
Venues (Conferences, Journals, ...)
|
|
GrowBag graphs for keyword ? (Num. hits/coverage)
Group by:
The graphs summarize 1960 occurrences of 846 keywords
|
|
|
Results
Found 3383 publication records. Showing 3383 according to the selection in the facets
Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
27 | Stéphane Fèvre, Dongming Wang 0001 |
Combining Algebraic Computing and Term-Rewriting for Geometry Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
AISC ![In: Artificial Intelligence and Symbolic Computation, International Conference AISC'98, Plattsburgh, New York, USA, September 16-18, 1998, Proceedings, pp. 145-156, 1998, Springer, 3-540-64960-3. The full citation details ...](Pics/full.jpeg) |
1998 |
DBLP DOI BibTeX RDF |
|
27 | Mitsuharu Yamamoto, Koichi Takahashi, Masami Hagiya, Shin-ya Nishizaki, Tetsuo Tamai |
Formalization of Graph Search Algorithms and Its Applications. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 11th International Conference, TPHOLs'98, Canberra, Australia, September 27 - October 1, 1998, Proceedings, pp. 479-496, 1998, Springer, 3-540-64987-5. The full citation details ...](Pics/full.jpeg) |
1998 |
DBLP DOI BibTeX RDF |
|
27 | Ulrich Kühler, Claus-Peter Wirth |
Conditional Equational Specifications of Data Types with Partial Operations for Inductive Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
RTA ![In: Rewriting Techniques and Applications, 8th International Conference, RTA-97, Sitges, Spain, June 2-5, 1997, Proceedings, pp. 38-52, 1997, Springer, 3-540-62950-5. The full citation details ...](Pics/full.jpeg) |
1997 |
DBLP DOI BibTeX RDF |
|
27 | Albert John Camilleri |
A Hybrid Approach to Verifying Liveness in a Symmetric Multi-Processor. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 10th International Conference, TPHOLs'97, Murray Hill, NJ, USA, August 19-22, 1997, Proceedings, pp. 49-67, 1997, Springer, 3-540-63379-0. The full citation details ...](Pics/full.jpeg) |
1997 |
DBLP DOI BibTeX RDF |
|
27 | Vincent Zammit |
A Comparative Study of Coq and HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 10th International Conference, TPHOLs'97, Murray Hill, NJ, USA, August 19-22, 1997, Proceedings, pp. 323-337, 1997, Springer, 3-540-63379-0. The full citation details ...](Pics/full.jpeg) |
1997 |
DBLP DOI BibTeX RDF |
|
27 | Saturnino F. Luz-Filho |
Grammar Specification in Categorial Logics and Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-13, 13th International Conference on Automated Deduction, New Brunswick, NJ, USA, July 30 - August 3, 1996, Proceedings, pp. 703-717, 1996, Springer, 3-540-61511-3. The full citation details ...](Pics/full.jpeg) |
1996 |
DBLP DOI BibTeX RDF |
Mechanisms (semantic tableaux) and Applications (computational liguistics) |
27 | Harald Ganzinger |
Saturation-Based Theorem Proving: Past Successes and Future Potential (Abstract). ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-13, 13th International Conference on Automated Deduction, New Brunswick, NJ, USA, July 30 - August 3, 1996, Proceedings, pp. 1, 1996, Springer, 3-540-61511-3. The full citation details ...](Pics/full.jpeg) |
1996 |
DBLP DOI BibTeX RDF |
|
27 | Thomas Hillenbrand, Arnim Buch, Roland Fettig |
On Gaining Efficiency in Completion-Based Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
RTA ![In: Rewriting Techniques and Applications, 7th International Conference, RTA-96, New Brunswick, NJ, USA, July 27-30, 1996, Proceedings, pp. 432-435, 1996, Springer, 3-540-61464-8. The full citation details ...](Pics/full.jpeg) |
1996 |
DBLP DOI BibTeX RDF |
|
27 | Don Syme |
A New Interface for HOL - Ideas, Issues and Implementation. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Higher Order Logic Theorem Proving and Its Applications, 8th International Workshop, Aspen Grove, UT, USA, September 11-14, 1995, Proceedings, pp. 324-339, 1995, Springer, 3-540-60275-5. The full citation details ...](Pics/full.jpeg) |
1995 |
DBLP DOI BibTeX RDF |
|
27 | E. Thomas Schubert, Sarah Mocas |
A Mechanized Logic for Secure Key Escrow Protocol Verification. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Higher Order Logic Theorem Proving and Its Applications, 8th International Workshop, Aspen Grove, UT, USA, September 11-14, 1995, Proceedings, pp. 308-323, 1995, Springer, 3-540-60275-5. The full citation details ...](Pics/full.jpeg) |
1995 |
DBLP DOI BibTeX RDF |
|
27 | David A. Plaisted |
The Search Efficiency of Theorem Proving Strategies. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-12, 12th International Conference on Automated Deduction, Nancy, France, June 26 - July 1, 1994, Proceedings, pp. 57-71, 1994, Springer, 3-540-58156-1. The full citation details ...](Pics/full.jpeg) |
1994 |
DBLP DOI BibTeX RDF |
|
27 | Ahmed Guergueb, Jean Mainguené, Marie-Françoise Roy |
Examples of Automatic Theorem Proving a Real Geometry. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ISSAC ![In: Proceedings of the International Symposium on Symbolic and Algebraic Computation, ISSAC '94, Oxford, UK, July 20-22, 1994, pp. 20-24, 1994, ACM, 0-89791-638-7. The full citation details ...](Pics/full.jpeg) |
1994 |
DBLP DOI BibTeX RDF |
|
27 | David A. Fura, Arun K. Somani |
Interval-Semantic Component Models and the Efficient Verification of Transaction-Level Circiut Behavior. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Higher Order Logic Theorem Proving and Its Applications, 7th International Workshop, Valletta, Malta, September 19-22, 1994, Proceedings, pp. 205-220, 1994, Springer, 3-540-58450-1. The full citation details ...](Pics/full.jpeg) |
1994 |
DBLP DOI BibTeX RDF |
|
27 | Mats Larsson |
An Engineering Approach to Formal Digital System Design. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Higher Order Logic Theorem Proving and Its Applications, 7th International Workshop, Valletta, Malta, September 19-22, 1994, Proceedings, pp. 300-315, 1994, Springer, 3-540-58450-1. The full citation details ...](Pics/full.jpeg) |
1994 |
DBLP DOI BibTeX RDF |
|
27 | Ching-Tsun Chou |
Mechanical Verification of Distributed Algorithms in Higher-Order Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Higher Order Logic Theorem Proving and Its Applications, 7th International Workshop, Valletta, Malta, September 19-22, 1994, Proceedings, pp. 158-176, 1994, Springer, 3-540-58450-1. The full citation details ...](Pics/full.jpeg) |
1994 |
DBLP DOI BibTeX RDF |
|
27 | Phillip J. Windley |
Specifying Instruction-Set Architectures in HOL: A Primer. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Higher Order Logic Theorem Proving and Its Applications, 7th International Workshop, Valletta, Malta, September 19-22, 1994, Proceedings, pp. 440-455, 1994, Springer, 3-540-58450-1. The full citation details ...](Pics/full.jpeg) |
1994 |
DBLP DOI BibTeX RDF |
|
27 | Marta Franová, Yves Kodratoff, Martine Gross |
Constructive Matching Methodology: Formally Creative or Intelligent Inductive Theorem Proving? ![Search on Bibsonomy](Pics/bibsonomy.png) |
ISMIS ![In: Methodologies for Intelligent Systems, 7th International Symposium, ISMIS '93, Trondheim, Norway, June 15-18, 1993, Proceedings, pp. 476-485, 1993, Springer, 3-540-56804-2. The full citation details ...](Pics/full.jpeg) |
1993 |
DBLP DOI BibTeX RDF |
|
27 | Jürgen Avenhaus, Jörg Denzinger |
Distributing Equational Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
RTA ![In: Rewriting Techniques and Applications, 5th International Conference, RTA-93, Montreal, Canada, June 16-18, 1993, Proceedings, pp. 62-76, 1993, Springer, 3-540-56868-9. The full citation details ...](Pics/full.jpeg) |
1993 |
DBLP DOI BibTeX RDF |
|
27 | Zheng Zhu, Jeffrey J. Joyce, Carl-Johan H. Seger |
Verification of the Tamarack-3 Microprocessor in a Hybrid Verification Environment. ![Search on Bibsonomy](Pics/bibsonomy.png) |
HUG ![In: Higher Order Logic Theorem Proving and its Applications, 6th International Workshop, HUG '93, Vancouver, BC, Canada, August 11-13, 1993, Proceedings, pp. 253-266, 1993, Springer, 3-540-57826-9. The full citation details ...](Pics/full.jpeg) |
1993 |
DBLP DOI BibTeX RDF |
|
27 | Peter B. Andrews, Matthew Bishop, Sunil Issar, Dan Nesmith, Frank Pfenning, Hongwei Xi |
TPS: An Interactive and Automatic Tool for Proving Theorems of Type Theory. ![Search on Bibsonomy](Pics/bibsonomy.png) |
HUG ![In: Higher Order Logic Theorem Proving and its Applications, 6th International Workshop, HUG '93, Vancouver, BC, Canada, August 11-13, 1993, Proceedings, pp. 366-370, 1993, Springer, 3-540-57826-9. The full citation details ...](Pics/full.jpeg) |
1993 |
DBLP DOI BibTeX RDF |
|
27 | Catia M. Angelo, Luc J. M. Claesen, Hugo De Man |
Degrees of Formality in Shallow Embedding Hardware Description Languages in HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
HUG ![In: Higher Order Logic Theorem Proving and its Applications, 6th International Workshop, HUG '93, Vancouver, BC, Canada, August 11-13, 1993, Proceedings, pp. 89-100, 1993, Springer, 3-540-57826-9. The full citation details ...](Pics/full.jpeg) |
1993 |
DBLP DOI BibTeX RDF |
|
27 | Newton C. A. da Costa, Lawrence J. Henschen, James J. Lu, V. S. Subrahmanian |
Automatic Theorem Proving in Paraconsistent Logics: Theory and Implementation. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: 10th International Conference on Automated Deduction, Kaiserslautern, FRG, July 24-27, 1990, Proceedings, pp. 72-86, 1990, Springer, 3-540-52885-7. The full citation details ...](Pics/full.jpeg) |
1990 |
DBLP DOI BibTeX RDF |
|
27 | Christoph Walther |
Many-Sorted Inferences in Automated Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Sorts and Types in Artificial Intelligence ![In: Sorts and Types in Artificial Intelligence, Workshop, Eringerfeld, FRG, April 24-26, 1989, Proceedings, pp. 18-48, 1989, Springer, 3-540-52337-5. The full citation details ...](Pics/full.jpeg) |
1989 |
DBLP DOI BibTeX RDF |
|
27 | Larry M. Hines |
Hyper-Chaining and Knowledge-Based Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: 9th International Conference on Automated Deduction, Argonne, Illinois, USA, May 23-26, 1988, Proceedings, pp. 469-486, 1988, Springer, 3-540-19343-X. The full citation details ...](Pics/full.jpeg) |
1988 |
DBLP DOI BibTeX RDF |
|
27 | John K. Dixon |
Z-Resolution: Theorem-Proving with Compiled Axioms. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. ACM ![In: J. ACM 20(1), pp. 127-147, 1973. The full citation details ...](Pics/full.jpeg) |
1973 |
DBLP DOI BibTeX RDF |
|
26 | Kenichi Yajima, Shoichi Morimoto, Daisuke Horie, Noor Sheila Azreen, Yuichi Goto, Jingde Cheng |
FORVEST: A Support Tool for Formal Verification of Security Specifications with ISO/IEC 15408. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ARES ![In: Proceedings of the The Forth International Conference on Availability, Reliability and Security, ARES 2009, March 16-19, 2009, Fukuoka, Japan, pp. 624-629, 2009, IEEE Computer Society, 978-1-4244-3572-2. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
|
26 | John M. Rushby |
Harnessing Disruptive Innovation in Formal Verification. ![Search on Bibsonomy](Pics/bibsonomy.png) |
SEFM ![In: Fourth IEEE International Conference on Software Engineering and Formal Methods (SEFM 2006), 11-15 September 2006, Pune, India, pp. 21-30, 2006, IEEE Computer Society, 0-7695-2678-0. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
|
26 | Julian Richardson |
A Semantics for Proof Plans with Applications to Interactive Proof Planning. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LPAR ![In: Logic for Programming, Artificial Intelligence, and Reasoning, 9th International Conference, LPAR 2002, Tbilisi, Georgia, October 14-18, 2002, Proceedings, pp. 337-351, 2002, Springer, 3-540-00010-0. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
|
26 | Manfred Kerber, Martin Pollet |
On the Design of Mathematical Concepts. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Australian Joint Conference on Artificial Intelligence ![In: AI 2002: Advances in Artificial Intelligence, 15th Australian Joint Conference on Artificial Intelligence, Canberra, Australia, December 2-6, 2002, Proceedings, pp. 716, 2002, Springer, 3-540-00197-2. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
|
26 | Constance L. Heitmeyer |
On the Need for Practical Formal Methods. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FTRTFT ![In: Formal Techniques in Real-Time and Fault-Tolerant Systems, 5th International Symposium, FTRTFT'98, Lyngby, Denmark, September 14-18, 1998, Proceedings, pp. 18-26, 1998, Springer, 3-540-65003-2. The full citation details ...](Pics/full.jpeg) |
1998 |
DBLP DOI BibTeX RDF |
|
26 | Robert Matzinger |
Computational Representations of Herbrand Models Using Grammars. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CSL ![In: Computer Science Logic, 10th International Workshop, CSL '96, Annual Conference of the EACSL, Utrecht, The Netherlands, September 21-27, 1996, Selected Papers, pp. 334-348, 1996, Springer, 3-540-63172-0. The full citation details ...](Pics/full.jpeg) |
1996 |
DBLP DOI BibTeX RDF |
|
26 | Ken Hirose |
An Approach to Proof Checker. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MFCS ![In: Mathematical Foundations of Computer Science 1986, Bratislava, Czechoslovakia, August 25-29, 1996, Proceedings, pp. 113-127, 1986, Springer, 3-540-16783-8. The full citation details ...](Pics/full.jpeg) |
1986 |
DBLP DOI BibTeX RDF |
|
26 | Nicola Olivetti, Gian Luca Pozzato |
Nested sequent calculi and theorem proving for normal conditional logics: The theorem prover NESCOND. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Intelligenza Artificiale ![In: Intelligenza Artificiale 9(2), pp. 109-125, 2015. The full citation details ...](Pics/full.jpeg) |
2015 |
DBLP DOI BibTeX RDF |
|
26 | Mark E. Stickel |
Automated theorem-proving research in the Fifth Generation Computer Systems Project: Model generation theorem provers. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Future Gener. Comput. Syst. ![In: Future Gener. Comput. Syst. 9(2), pp. 143-152, 1993. The full citation details ...](Pics/full.jpeg) |
1993 |
DBLP DOI BibTeX RDF |
|
25 | Edwin C. Brady |
Ivor, a Proof Engine. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IFL ![In: Implementation and Application of Functional Languages, 18th International Symp osium, IFL 2006, Budapest, Hungary, September 4-6, 2006, Revised Selected Papers, pp. 145-162, 2006, Springer, 978-3-540-74129-9. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
|
25 | Tarek Mhamdi, Sofiène Tahar |
Providing Automated Verification in HOL Using MDGs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ATVA ![In: Automated Technology for Verification and Analysis: Second International Conference, ATVA 2004, Taipei, Taiwan, ROC, October 31-November 3, 2004. Proceedings, pp. 278-293, 2004, Springer, 3-540-23610-4. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
25 | Andrei Voronkov |
Algorithms, Datastructures, and other Issues in Efficient Automated Deduction. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IJCAR ![In: Automated Reasoning, First International Joint Conference, IJCAR 2001, Siena, Italy, June 18-23, 2001, Proceedings, pp. 13-28, 2001, Springer, 3-540-42254-4. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
|
25 | Christoph Lüth, Burkhart Wolff |
More About TAS and IsaWin - Tools for Formal Program Development. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FASE ![In: Fundamental Approaches to Software Engineering, Third Internationsl Conference, FASE 2000, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS 2000, Berlin, Germany, March 25 - April 2, 2000, Proceedings, pp. 367-370, 2000, Springer, 3-540-67261-3. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
|
24 | Deepak Kapur, Balakrishnan Krishnamurthy |
A Natural Proof System Based on rewriting Techniques. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: 7th International Conference on Automated Deduction, Napa, California, USA, May 14-16, 1984, Proceedings, pp. 53-64, 1984, Springer, 3-540-96022-8. The full citation details ...](Pics/full.jpeg) |
1984 |
DBLP DOI BibTeX RDF |
|
24 | Lawrence J. Henschen, Larry Wos |
Unit Refutations and Horn Sets. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. ACM ![In: J. ACM 21(4), pp. 590-605, 1974. The full citation details ...](Pics/full.jpeg) |
1974 |
DBLP DOI BibTeX RDF |
|
22 | Myla Archer, Hongping Lim, Nancy A. Lynch, Sayan Mitra, Shinya Umeno |
Specifying and proving properties of timed I/O automata in the TIOA toolkit. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MEMOCODE ![In: 4th ACM & IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE 2006), 27-29 July 2006, Embassy Suites, Napa, California, USA, pp. 129-138, 2006, IEEE Computer Society, 1-4244-0421-5. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
|
22 | Ralph D. Jeffords, Constance L. Heitmeyer |
A strategy for efficiently verifying requirements. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ESEC / SIGSOFT FSE ![In: Proceedings of the 11th ACM SIGSOFT Symposium on Foundations of Software Engineering 2003 held jointly with 9th European Software Engineering Conference, ESEC/FSE 2003, Helsinki, Finland, September 1-5, 2003, pp. 28-37, 2003, ACM, 978-1-58113-743-9. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
model checking, formal methods, software tools, invariants, requirements specification, compositional verification |
21 | Warren A. Hunt Jr., Sol Swords |
Centaur Technology Media Unit Verification. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CAV ![In: Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings, pp. 353-367, 2009, Springer, 978-3-642-02657-7. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
|
21 | Timothy L. Hinrichs |
Extensional Reasoning. ![Search on Bibsonomy](Pics/bibsonomy.png) |
SARA ![In: Abstraction, Reformulation, and Approximation, 7th International Symposium, SARA 2007, Whistler, Canada, July 18-21, 2007, Proceedings, pp. 400-401, 2007, Springer, 978-3-540-73579-3. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
|
21 | Xia Wu, Jigui Sun, Kun Hou |
An Extension Rule Based First-Order Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
KSEM ![In: Knowledge Science, Engineering and Management, First International Conference, KSEM 2006, Guilin, China, August 5-8, 2006, Proceedings, pp. 514-524, 2006, Springer, 3-540-37033-1. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
|
21 | John M. Rushby |
Tutorial: Automated Formal Methods with PVS, SAL, and Yices. ![Search on Bibsonomy](Pics/bibsonomy.png) |
SEFM ![In: Fourth IEEE International Conference on Software Engineering and Formal Methods (SEFM 2006), 11-15 September 2006, Pune, India, pp. 262, 2006, IEEE Computer Society, 0-7695-2678-0. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
|
21 | Stefano Brait, Franco Fummi, Graziano Pravadelli |
On the use of a high-level fault model to analyze logical consequence of properties. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MEMOCODE ![In: 3rd ACM & IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE 2005), 11-14 July 2005, Verona, Italy, Proceedings, pp. 221-230, 2005, IEEE Computer Society, 0-7803-9227-2. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
|
21 | Thomas Raths, Jens Otten, Christoph Kreitz |
The ILTP Library: Benchmarking Automated Theorem Provers for Intuitionistic Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TABLEAUX ![In: Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX 2005, Koblenz, Germany, September 14-17, 2005, Proceedings, pp. 333-337, 2005, Springer, 3-540-28931-3. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
|
21 | Christoph Benzmüller, Volker Sorge, Mateja Jamnik, Manfred Kerber |
Can a Higher-Order and a First-Order Theorem Prover Cooperate?. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LPAR ![In: Logic for Programming, Artificial Intelligence, and Reasoning, 11th International Conference, LPAR 2004, Montevideo, Uruguay, March 14-18, 2005, Proceedings, pp. 415-431, 2004, Springer, 3-540-25236-3. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
21 | Ullrich Hustadt, Boris Motik, Ulrike Sattler |
A Decomposition Rule for Decision Procedures by Resolution-Based Calculi. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LPAR ![In: Logic for Programming, Artificial Intelligence, and Reasoning, 11th International Conference, LPAR 2004, Montevideo, Uruguay, March 14-18, 2005, Proceedings, pp. 21-35, 2004, Springer, 3-540-25236-3. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
21 | Vu Ha, Murali Rangarajan, Darren D. Cofer, Harald Rueß, Bruno Dutertre |
Feature-Based Decomposition of Inductive Proofs Applied to Real-Time Avionics Software: An Experience Report. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICSE ![In: 26th International Conference on Software Engineering (ICSE 2004), 23-28 May 2004, Edinburgh, United Kingdom, pp. 304-313, 2004, IEEE Computer Society, 0-7695-2163-0. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
21 | Konstantine Arkoudas, Selmer Bringsjord |
Metareasoning for Multi-agent Epistemic Logics. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CLIMA ![In: Computational Logic in Multi-Agent Systems, 5th International Workshop, CLIMA V, Lisbon, Portugal, September 29-30, 2004, Revised Selected and Invited Papers, pp. 111-125, 2004, Springer, 3-540-28060-X. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
21 | Jürgen Avenhaus, Ulrich Kühler, Tobias Schmidt-Samoa, Claus-Peter Wirth |
How to Prove Inductive Theorems? QUODLIBET! ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-19, 19th International Conference on Automated Deduction Miami Beach, FL, USA, July 28 - August 2, 2003, Proceedings, pp. 328-333, 2003, Springer, 3-540-40559-3. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
|
21 | Steve Roach, Jeffrey Van Baalen |
Experience Report on Automated Procedure Construction for Deductive Synthesis. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ASE ![In: 17th IEEE International Conference on Automated Software Engineering (ASE 2002), 23-27 September 2002, Edinburgh, Scotland, UK, pp. 69-, 2002, IEEE Computer Society, 0-7695-1736-6. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
|
21 | V. K. Pisini, Sofiène Tahar, Paul Curzon, Otmane Aït Mohamed, Xiaoyu Song |
Formal hardware verification by integrating HOL and MDG. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACM Great Lakes Symposium on VLSI ![In: Proceedings of the 10th ACM Great Lakes Symposium on VLSI 2000, Chicago, Illinois, USA, March 2-4, 2000, pp. 23-28, 2000, ACM, 1-58113-251-4. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
|
21 | Ingo Dahn |
Interpretation of a Mizar-Like Logic in First-Order Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FTP (LNCS Selection) ![In: Automated Deduction in Classical and Non-Classical Logics, Selected Papers, pp. 137-151, 1998, Springer, 3-540-67190-0. The full citation details ...](Pics/full.jpeg) |
1998 |
DBLP DOI BibTeX RDF |
|
21 | Gilles Défourneaux, Nicolas Peltier |
Partial Matching for Analogy Discovery in Proofs and Counter-Examples. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-14, 14th International Conference on Automated Deduction, Townsville, North Queensland, Australia, July 13-17, 1997, Proceedings, pp. 431-445, 1997, Springer, 3-540-63104-6. The full citation details ...](Pics/full.jpeg) |
1997 |
DBLP DOI BibTeX RDF |
|
21 | Koji Iwanuma |
Lemma Matching for a PTTP-based Top-down Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-14, 14th International Conference on Automated Deduction, Townsville, North Queensland, Australia, July 13-17, 1997, Proceedings, pp. 146-160, 1997, Springer, 3-540-63104-6. The full citation details ...](Pics/full.jpeg) |
1997 |
DBLP DOI BibTeX RDF |
|
21 | Alan M. Frisch, Richard B. Scherl |
A Constraint Logic Approach to Modal Deduction. ![Search on Bibsonomy](Pics/bibsonomy.png) |
JELIA ![In: Logics in AI, European Workshop, JELIA '90, Amsterdam, The Netherlands, September 10-14, 1990, Proceedings, pp. 234-250, 1990, Springer, 3-540-53686-8. The full citation details ...](Pics/full.jpeg) |
1990 |
DBLP DOI BibTeX RDF |
|
21 | David A. Schmidt |
A Programming Notation for Tactical Reasoning. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: 7th International Conference on Automated Deduction, Napa, California, USA, May 14-16, 1984, Proceedings, pp. 445-459, 1984, Springer, 3-540-96022-8. The full citation details ...](Pics/full.jpeg) |
1984 |
DBLP DOI BibTeX RDF |
|
21 | Petros Papapanagiotou, Jacques D. Fleuriot |
Formal Verification of Web Services Composition Using Linear Logic and the pi-calculus. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ECOWS ![In: 9th IEEE European Conference on Web Services, ECOWS 2011, Lugano, Switzerland, September 14-16, 2011, pp. 31-38, 2011, IEEE, 978-1-4577-1532-7. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
proofs-as-processes, Web Services, formal verification, theorem proving, services composition |
21 | Hui Kong 0004, Hehua Zhang, Xiaoyu Song, Ming Gu 0001, Jiaguang Sun 0001 |
Proving Computational Geometry Algorithms in TLA+2. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TASE ![In: 5th IEEE International Symposium on Theoretical Aspects of Software Engineering, TASE 2011, Xi'an, China, 29-31 August 2011, pp. 251-254, 2011, IEEE Computer Society, 978-1-4577-1487-0. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
algorithm verification, TLA+2, geometry algorithm, theorem proving, loop invariant |
21 | Florian Haftmann |
From higher-order logic to Haskell: there and back again. ![Search on Bibsonomy](Pics/bibsonomy.png) |
PEPM ![In: Proceedings of the 2010 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM 2010, Madrid, Spain, January 18-19, 2010, pp. 155-158, 2010, ACM, 978-1-60558-727-1. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
code generation, theorem proving, haskell, higher-order logic, isabelle |
21 | Sander Vermolen, Jozef Hooman, Peter Gorm Larsen |
Proving consistency of VDM models using HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
SAC ![In: Proceedings of the 2010 ACM Symposium on Applied Computing (SAC), Sierre, Switzerland, March 22-26, 2010, pp. 2503-2510, 2010, ACM, 978-1-60558-639-7. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
verification, theorem proving, VDM, HOL, model consistency |
21 | Tuan Minh Pham |
Similar triangles and orientation in plane elementary geometry for Coq-based proofs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
SAC ![In: Proceedings of the 2010 ACM Symposium on Applied Computing (SAC), Sierre, Switzerland, March 22-26, 2010, pp. 1268-1269, 2010, ACM, 978-1-60558-639-7. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
similar triangles, orientation, formalization, Coq, geometric theorem proving |
21 | Simon Meier, Cas Cremers, David A. Basin |
Strong Invariants for the Efficient Construction of Machine-Checked Protocol Security Proofs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CSF ![In: Proceedings of the 23rd IEEE Computer Security Foundations Symposium, CSF 2010, Edinburgh, United Kingdom, July 17-19, 2010, pp. 231-245, 2010, IEEE Computer Society, 978-0-7695-4082-5. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
formal methods, theorem proving, security protocols, automatic tools |
21 | Asma Moubaiddin, Nadim Obeid |
Partial information basis for agent-based collaborative dialogue. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Appl. Intell. ![In: Appl. Intell. 30(2), pp. 142-167, 2009. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
Partial information states, Agent, Theorem proving, Argument, Dialogue, Three-valued logic, Nonmonotonic |
21 | Giorgio Dalzotto, Tomás Recio |
On Protocols for the Automated Discovery of Theorems in Elementary Geometry. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 43(2), pp. 203-236, 2009. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
Automatic theorem discovery, Elementary geometry, Computational algebraic geometry, Automatic theorem proving |
21 | Magnus Björk |
First Order Stålmarck. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 42(1), pp. 99-122, 2009. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
Stålmarck’s method, Universal lemmas, First order logic, Automated theorem proving, Intersections |
21 | Harvey Tuch |
Formal Verification of C Systems Code. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 42(2-4), pp. 125-187, 2009. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
C, Separation logic, Interactive theorem proving |
21 | Matthias Daum 0001, Jan Dörrenbächer, Burkhart Wolff |
Proving Fairness and Implementation Correctness of a Microkernel Scheduler. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 42(2-4), pp. 349-388, 2009. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
Formal verification, Interactive theorem proving, Microkernel, Isabelle/HOL |
21 | Marcel Oliveira, Ana Cavalcanti 0001, Jim Woodcock 0001 |
A UTP semantics for Circus. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Formal Aspects Comput. ![In: Formal Aspects Comput. 21(1-2), pp. 3-32, 2009. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
Concurrency, Theorem proving, Relational model, Refinement calculus |
21 | Jens Bendisposto, Michael Leuschel |
Proof Assisted Model Checking for B. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICFEM ![In: Formal Methods and Software Engineering, 11th International Conference on Formal Engineering Methods, ICFEM 2009, Rio de Janeiro, Brazil, December 9-12, 2009. Proceedings, pp. 504-520, 2009, Springer, 978-3-642-10372-8. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
Model Checking, Experiment, Theorem Proving, B-Method, Tool Integration |
21 | André Platzer, Jan-David Quesel |
European Train Control System: A Case Study in Formal Verification. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICFEM ![In: Formal Methods and Software Engineering, 11th International Conference on Formal Engineering Methods, ICFEM 2009, Rio de Janeiro, Brazil, December 9-12, 2009. Proceedings, pp. 246-265, 2009, Springer, 978-3-642-10372-8. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
formal verification of hybrid systems, train control, parameter constraint identification, theorem proving, disturbances |
21 | Faranak Heidarian, Julien Schmaltz, Frits W. Vaandrager |
Analysis of a Clock Synchronization Protocol for Wireless Sensor Networks. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FM ![In: FM 2009: Formal Methods, Second World Congress, Eindhoven, The Netherlands, November 2-6, 2009. Proceedings, pp. 516-531, 2009, Springer, 978-3-642-05088-6. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
wireless sensor networks, model checking, theorem proving, timed automata, clock synchronization, industrial application |
21 | Levent Erkök, John Matthews |
Pragmatic equivalence and safety checking in Cryptol. ![Search on Bibsonomy](Pics/bibsonomy.png) |
PLPV ![In: Proceedings of the 3rd ACM Workshop Programming Languages meets Program Verification, PLPV 2009, Savannah, GA, USA, January 20, 2009, pp. 73-82, 2009, ACM, 978-1-60558-330-3. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
sat/smt solving, size polymorphism, formal methods, cryptography, theorem proving, equivalence checking |
21 | Amy P. Felty, Alberto Momigliano |
Reasoning with hypothetical judgments and open terms in hybrid. ![Search on Bibsonomy](Pics/bibsonomy.png) |
PPDP ![In: Proceedings of the 11th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, September 7-9, 2009, Coimbra, Portugal, pp. 83-92, 2009, ACM, 978-1-60558-568-0. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
name-binding, induction, logical frameworks, higher-order abstract syntax, interactive theorem proving |
21 | Xiaolei Gao, Huaikou Miao |
Proving Total Correctness of Refinement Based on Tableau. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ISPA ![In: IEEE International Symposium on Parallel and Distributed Processing with Applications, ISPA 2009, Chengdu, Sichuan, China, 10-12 August 2009, pp. 702-707, 2009, IEEE Computer Society, 978-0-7695-3747-4. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
Tableau method, Specification, refinement, theorem proving, Program Synthesis, total correctness |
21 | Jorge F. Salas |
A Language for Encoding and Reconstruction of Rewriting Proofs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
SCCC ![In: 2009 International Conference of the Chilean Computer Science Society, SCCC 2009, Santiago, Chile, November 10-12, 2009, pp. 67-74, 2009, IEEE Computer Society, 978-0-7695-4137-2. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
Semiautomated theorem proving, encoding languages for proofs, rewriting induction, rewriting systems |
21 | Achim D. Brucker, Burkhart Wolff |
hol-TestGen. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FASE ![In: Fundamental Approaches to Software Engineering, 12th International Conference, FASE 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings, pp. 417-420, 2009, Springer, 978-3-642-00592-3. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
symbolic test-case generations, theorem proving, black box testing, white box testing, interactive testing |
21 | Helmut Seidl, Kumar Neeraj Verma |
Flat and one-variable clauses: Complexity of verifying cryptographic protocols with single blind copying. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACM Trans. Comput. Log. ![In: ACM Trans. Comput. Log. 9(4), pp. 28:1-28:45, 2008. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
instantiation-based theorem proving, Cryptographic protocols, first-order logic, resolution, Horn clauses |
21 | Susanne Graf |
OMEGA: correct development of real time and embedded systems. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Softw. Syst. Model. ![In: Softw. Syst. Model. 7(2), pp. 127-130, 2008. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
Support for object oriented, Component-based system design, Model checking, UML, Embedded systems, Real time, Theorem proving, Type-checking, Model-based |
21 | Marc Bezem, Dimitri Hendriks |
On the Mechanization of the Proof of Hessenberg's Theorem in Coherent Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 40(1), pp. 61-85, 2008. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
Coherent logic, Proof objects, Hessenberg’s theorem, Automated theorem proving |
21 | Achim D. Brucker, Burkhart Wolff |
An Extensible Encoding of Object-oriented Data Models in hol. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 41(3-4), pp. 219-249, 2008. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
Verification, Theorem proving, Object-oriented data models, hol |
21 | Sandip Ray, Warren A. Hunt Jr., John Matthews, J Strother Moore |
A Mechanical Analysis of Program Verification Strategies. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 40(4), pp. 245-269, 2008. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
Inductive assertions, Partial correctness, Theorem proving, Invariants, Total correctness |
21 | Hasan Amjad |
Data Compression for Proof Replay. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 41(3-4), pp. 193-218, 2008. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
Proof translation, Interactive theorem proving, SAT solvers |
21 | André Platzer |
Differential Dynamic Logic for Hybrid Systems. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 41(2), pp. 143-189, 2008. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
Verification of hybrid systems, Differential equations, Automated theorem proving, Dynamic logic, Sequent calculus, Axiomatisation |
21 | Asem Kasem, Tetsuo Ida |
Computational origami environment on the web. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Frontiers Comput. Sci. China ![In: Frontiers Comput. Sci. China 2(1), pp. 39-54, 2008. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
computational origami, symbolic web services, origami theorem proving, symbolic computation |
21 | Leo Freitas, Jim Woodcock 0001 |
Mechanising Mondex with Z/Eves. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Formal Aspects Comput. ![In: Formal Aspects Comput. 20(1), pp. 117-139, 2008. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
Electronic finance, Grand Challenge in Verified Software, Software archaeology, Z/Eves, Security, Verification, Refinement, Theorem proving, Smart cards, Correctness, Z notation, Grand challenges, Verified Software Repository, Mondex |
21 | Jim Woodcock 0001, Susan Stepney, David Cooper, John A. Clark, Jeremy Jacob |
The certification of the Mondex electronic purse to ITSEC Level E6. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Formal Aspects Comput. ![In: Formal Aspects Comput. 20(1), pp. 5-19, 2008. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
Electronic finance, Grand Challenge in Verified Software, ITSEC Level E6, Security, Verification, Refinement, Theorem proving, Smart cards, Certification, Correctness, Z notation, Grand challenges, Verified Software Repository, Mondex |
21 | Florian Kammüller |
Formalizing non-interference for a simple bytecode language in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Formal Aspects Comput. ![In: Formal Aspects Comput. 20(3), pp. 259-275, 2008. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
Formal methods for security, Programming language analysis, Interactive theorem proving, Modular specification |
21 | Andriy Dunets, Gerhard Schellhorn, Wolfgang Reif |
Automating Algebraic Specifications of Non-freely Generated Data Types. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ATVA ![In: Automated Technology for Verification and Analysis, 6th International Symposium, ATVA 2008, Seoul, Korea, October 20-23, 2008. Proceedings, pp. 141-155, 2008, Springer, 978-3-540-88386-9. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
SAT checking, theorem proving, first-order logic, abstract data types, Algebraic specifications, finite models |
21 | Dominique Borrione, Amr Helmy, Laurence Pierre, Julien Schmaltz |
Executable formal specification and validation of NoC communication infrastructures. ![Search on Bibsonomy](Pics/bibsonomy.png) |
SBCCI ![In: Proceedings of the 21st Annual Symposium on Integrated Circuits and Systems Design, SBCCI 2008, Gramado, Brazil, September 1-4, 2008, pp. 176-181, 2008, ACM, 978-1-60558-231-3. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
simulation, verification, theorem proving |
21 | Ewen Denney, Bernd Fischer 0002 |
Generating customized verifiers for automatically generated code. ![Search on Bibsonomy](Pics/bibsonomy.png) |
GPCE ![In: Generative Programming and Component Engineering, 7th International Conference, GPCE 2008, Nashville, TN, USA, October 19-23, 2008, Proceedings, pp. 77-88, 2008, ACM, 978-1-60558-267-2. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
logical annotations, program verification, automated theorem proving, hoare logic, software certification, automated code generation |
21 | Wendy Verbruggen, Edsko de Vries, Arthur Hughes |
Polytypic programming in COQ. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICFP-WGP ![In: Proceedings of the ACM SIGPLAN Workshop on Generic Programming, WGP 2008, Victoria, BC, Canada, September 20, 2008, pp. 49-60, 2008, ACM, 978-1-60558-060-9. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
kind-indexed types, theorem proving, generic programming, formalization, coq, polytypic programming |
21 | Alexander Krauss 0001 |
Pattern minimization problems over recursive data types. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICFP ![In: Proceeding of the 13th ACM SIGPLAN international conference on Functional programming, ICFP 2008, Victoria, BC, Canada, September 20-28, 2008, pp. 267-274, 2008, ACM, 978-1-59593-919-7. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
complexity, pattern matching, theorem proving |
21 | André Platzer, Jan-David Quesel |
KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description). ![Search on Bibsonomy](Pics/bibsonomy.png) |
IJCAR ![In: Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings, pp. 171-178, 2008, Springer, 978-3-540-71069-1. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
verification of hybrid systems, decision procedures, computer algebra, automated theorem proving, dynamic logic |
21 | John Derrick, Gerhard Schellhorn, Heike Wehrheim |
Mechanizing a Correctness Proof for a Lock-Free Concurrent Stack. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FMOODS ![In: Formal Methods for Open Object-Based Distributed Systems, 10th IFIP WG 6.1 International Conference, FMOODS 2008, Oslo, Norway, June 4-6, 2008, Proceedings, pp. 78-95, 2008, Springer, 978-3-540-68862-4. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
non-atomic refinement, KIV, refinement, theorem proving, Z, linearizability, concurrent access |
21 | Chunqing Chen, Jin Song Dong, Jun Sun 0001 |
A verification system for timed interval calculus. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICSE ![In: 30th International Conference on Software Engineering (ICSE 2008), Leipzig, Germany, May 10-18, 2008, pp. 271-280, 2008, ACM, 978-1-60558-079-1. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
real-time systems, theorem proving, specification language, pvs |
21 | Lucas Dixon, Ross Duncan |
Extending Graphical Representations for Compact Closed Categories with Applications to Symbolic Quantum Computation. ![Search on Bibsonomy](Pics/bibsonomy.png) |
AISC/MKM/Calculemus ![In: Intelligent Computer Mathematics, 9th International Conference, AISC 2008, 15th Symposium, Calculemus 2008, 7th International Conference, MKM 2008, Birmingham, UK, July 28 - August 1, 2008. Proceedings, pp. 77-92, 2008, Springer, 978-3-540-85109-7. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
categorical logic, graphical calculi, quantum computing, graph rewriting, interactive theorem proving |
Displaying result #301 - #400 of 3383 (100 per page; Change: ) Pages: [ <<][ 1][ 2][ 3][ 4][ 5][ 6][ 7][ 8][ 9][ 10][ 11][ 12][ 13][ >>] |
|