|
|
Venues (Conferences, Journals, ...)
|
|
GrowBag graphs for keyword ? (Num. hits/coverage)
Group by:
The graphs summarize 4202 occurrences of 1987 keywords
|
|
|
Results
Found 7488 publication records. Showing 7488 according to the selection in the facets
Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
52 | Zohar Manna, Stephen Nes, Jean Vuillemin |
Inductive methods for proving properties of programs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Proving Assertions About Programs ![In: Proceedings of ACM Conference on Proving Assertions About Programs, Las Cruces, New Mexico, USA, January 6-7, 1972, pp. 27-50, 1972, ACM, 978-1-4503-7891-8. The full citation details ...](Pics/full.jpeg) |
1972 |
DBLP DOI BibTeX RDF |
|
47 | Quan Liu, Yang Gao 0001, Zhiming Cui, WangShu Yao, ZhongWen Chen |
An Tableau Automated Theorem Proving Method Using Logical Reinforcement Learning. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ISICA ![In: Advances in Computation and Intelligence, Second International Symposium, ISICA 2007, Wuhan, China, September 21-23, 2007, Proceedings, pp. 262-270, 2007, Springer, 978-3-540-74580-8. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
logical reinforcement learning, tableau automated theorem proving, LOMDP |
44 | Tsong Yueh Chen, T. H. Tse, Zhiquan Zhou |
Semi-proving: an integrated method based on global symbolic evaluation and metamorphic testing. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ISSTA ![In: Proceedings of the International Symposium on Software Testing and Analysis, ISSTA 2002, Roma, Italy, July 22-24, 2002, pp. 191-195, 2002, ACM, 1-58113-562-9. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
global symbolic evaluation, program proving, semi-proving, program testing, symbolic execution, metamorphic testing |
42 | Sandip Ray, Rob Sumners |
Combining Theorem Proving with Model Checking through Predicate Abstraction. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Des. Test Comput. ![In: IEEE Des. Test Comput. 24(2), pp. 132-139, 2007. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
model checking, formal verification, theorem proving, predicate abstraction, ACL2 |
42 | Youngsik Kim, Parija Sule, Nazanin Mansouri |
Exploiting PSL standard assertions in a theorem-proving-based verification environment. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACM Great Lakes Symposium on VLSI ![In: Proceedings of the 15th ACM Great Lakes Symposium on VLSI 2005, Chicago, Illinois, USA, April 17-19, 2005, pp. 400-403, 2005, ACM, 1-59593-057-4. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
assertion-based design, modeling, verification, theorem-proving, formal semantics, PSL |
42 | Sun Yong-qiang, Lu Ru-zhan, Bi Hua |
Program synthesis based on Boyer-Moore theorem proving techniques. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACM Conference on Computer Science ![In: Proceedings of the 13th ACM Annual Conference on Computer Science, New Orleans, Louisiana, USA, 1985, pp. 348-355, 1985, ACM, 0-89791-150-4. The full citation details ...](Pics/full.jpeg) |
1985 |
DBLP DOI BibTeX RDF |
Boyer-Moore technique, program sysnthesis, theorem proving, resolution |
41 | |
Proceedings of ACM Conference on Proving Assertions About Programs, Las Cruces, New Mexico, USA, January 6-7, 1972 ![Search on Bibsonomy](Pics/bibsonomy.png) |
Proving Assertions About Programs ![ACM, 978-1-4503-7891-8 The full citation details ...](Pics/full.jpeg) |
1972 |
DBLP DOI BibTeX RDF |
|
41 | Michel Sintzoff |
Calculating properties of programs by valuations on specific models. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Proving Assertions About Programs ![In: Proceedings of ACM Conference on Proving Assertions About Programs, Las Cruces, New Mexico, USA, January 6-7, 1972, pp. 203-207, 1972, ACM, 978-1-4503-7891-8. The full citation details ...](Pics/full.jpeg) |
1972 |
DBLP DOI BibTeX RDF |
|
41 | Cliff B. Jones |
Formal development of correct algorithms: An example based on earley's recogniser. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Proving Assertions About Programs ![In: Proceedings of ACM Conference on Proving Assertions About Programs, Las Cruces, New Mexico, USA, January 6-7, 1972, pp. 150-169, 1972, ACM, 978-1-4503-7891-8. The full citation details ...](Pics/full.jpeg) |
1972 |
DBLP DOI BibTeX RDF |
|
41 | Robin Milner |
Implementation and applications of Scott's logic for computable functions. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Proving Assertions About Programs ![In: Proceedings of ACM Conference on Proving Assertions About Programs, Las Cruces, New Mexico, USA, January 6-7, 1972, pp. 1-6, 1972, ACM, 978-1-4503-7891-8. The full citation details ...](Pics/full.jpeg) |
1972 |
DBLP DOI BibTeX RDF |
|
41 | Clement L. McGowan |
The "most recent" error: Its causes and correction. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Proving Assertions About Programs ![In: Proceedings of ACM Conference on Proving Assertions About Programs, Las Cruces, New Mexico, USA, January 6-7, 1972, pp. 191-202, 1972, ACM, 978-1-4503-7891-8. The full citation details ...](Pics/full.jpeg) |
1972 |
DBLP DOI BibTeX RDF |
|
41 | Peter Wegner |
Operational semantics of programming languages. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Proving Assertions About Programs ![In: Proceedings of ACM Conference on Proving Assertions About Programs, Las Cruces, New Mexico, USA, January 6-7, 1972, pp. 128-141, 1972, ACM, 978-1-4503-7891-8. The full citation details ...](Pics/full.jpeg) |
1972 |
DBLP DOI BibTeX RDF |
|
41 | Clement McGowan |
The Contour Model Lambda Calculus Machine. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Proving Assertions About Programs ![In: Proceedings of ACM Conference on Proving Assertions About Programs, Las Cruces, New Mexico, USA, January 6-7, 1972, pp. 110-115, 1972, ACM, 978-1-4503-7891-8. The full citation details ...](Pics/full.jpeg) |
1972 |
DBLP DOI BibTeX RDF |
|
41 | Daniel M. Berry |
The equivalence of models of tasking. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Proving Assertions About Programs ![In: Proceedings of ACM Conference on Proving Assertions About Programs, Las Cruces, New Mexico, USA, January 6-7, 1972, pp. 170-190, 1972, ACM, 978-1-4503-7891-8. The full citation details ...](Pics/full.jpeg) |
1972 |
DBLP DOI BibTeX RDF |
|
41 | Jean-Marie Cadiou, Zohar Manna |
Recursive definitions of partial functions and their computations. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Proving Assertions About Programs ![In: Proceedings of ACM Conference on Proving Assertions About Programs, Las Cruces, New Mexico, USA, January 6-7, 1972, pp. 58-65, 1972, ACM, 978-1-4503-7891-8. The full citation details ...](Pics/full.jpeg) |
1972 |
DBLP DOI BibTeX RDF |
|
41 | Michael J. Fischer |
Lambda calculus schemata. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Proving Assertions About Programs ![In: Proceedings of ACM Conference on Proving Assertions About Programs, Las Cruces, New Mexico, USA, January 6-7, 1972, pp. 104-109, 1972, ACM, 978-1-4503-7891-8. The full citation details ...](Pics/full.jpeg) |
1972 |
DBLP DOI BibTeX RDF |
|
41 | Stephen J. Garland, David C. Luckham |
Translating recursion schemes into program schemes. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Proving Assertions About Programs ![In: Proceedings of ACM Conference on Proving Assertions About Programs, Las Cruces, New Mexico, USA, January 6-7, 1972, pp. 83-96, 1972, ACM, 978-1-4503-7891-8. The full citation details ...](Pics/full.jpeg) |
1972 |
DBLP DOI BibTeX RDF |
|
41 | John A. N. Lee |
The definition and validation of the radix sorting technique. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Proving Assertions About Programs ![In: Proceedings of ACM Conference on Proving Assertions About Programs, Las Cruces, New Mexico, USA, January 6-7, 1972, pp. 142-149, 1972, ACM, 978-1-4503-7891-8. The full citation details ...](Pics/full.jpeg) |
1972 |
DBLP DOI BibTeX RDF |
|
41 | C. David Allen |
Derivation of axiomatic definitions of programming languages from algorithmic definitions. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Proving Assertions About Programs ![In: Proceedings of ACM Conference on Proving Assertions About Programs, Las Cruces, New Mexico, USA, January 6-7, 1972, pp. 15-26, 1972, ACM, 978-1-4503-7891-8. The full citation details ...](Pics/full.jpeg) |
1972 |
DBLP DOI BibTeX RDF |
|
41 | Edward A. Ashcroft |
Program correctness methods and language definition. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Proving Assertions About Programs ![In: Proceedings of ACM Conference on Proving Assertions About Programs, Las Cruces, New Mexico, USA, January 6-7, 1972, pp. 51-57, 1972, ACM, 978-1-4503-7891-8. The full citation details ...](Pics/full.jpeg) |
1972 |
DBLP DOI BibTeX RDF |
|
41 | Michael S. Paterson |
Decision problems in computational models. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Proving Assertions About Programs ![In: Proceedings of ACM Conference on Proving Assertions About Programs, Las Cruces, New Mexico, USA, January 6-7, 1972, pp. 74-82, 1972, ACM, 978-1-4503-7891-8. The full citation details ...](Pics/full.jpeg) |
1972 |
DBLP DOI BibTeX RDF |
|
41 | Raymond E. Miller |
A boundary between decidability and undecidability for parallel program schemata (Extended Abstract). ![Search on Bibsonomy](Pics/bibsonomy.png) |
Proving Assertions About Programs ![In: Proceedings of ACM Conference on Proving Assertions About Programs, Las Cruces, New Mexico, USA, January 6-7, 1972, pp. 116-120, 1972, ACM, 978-1-4503-7891-8. The full citation details ...](Pics/full.jpeg) |
1972 |
DBLP DOI BibTeX RDF |
|
41 | Thomas E. Hull, Wayne H. Enright, Arthur E. Sedgwick |
The correctness of numerical algorithms. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Proving Assertions About Programs ![In: Proceedings of ACM Conference on Proving Assertions About Programs, Las Cruces, New Mexico, USA, January 6-7, 1972, pp. 66-73, 1972, ACM, 978-1-4503-7891-8. The full citation details ...](Pics/full.jpeg) |
1972 |
DBLP DOI BibTeX RDF |
|
41 | Ralph L. London |
Correctness of a compiler for a Lisp subset. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Proving Assertions About Programs ![In: Proceedings of ACM Conference on Proving Assertions About Programs, Las Cruces, New Mexico, USA, January 6-7, 1972, pp. 121-127, 1972, ACM, 978-1-4503-7891-8. The full citation details ...](Pics/full.jpeg) |
1972 |
DBLP DOI BibTeX RDF |
|
41 | Thomas E. Cheatham Jr., Ben Wegbreit |
On a laboratory for the study of automating programming. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Proving Assertions About Programs ![In: Proceedings of ACM Conference on Proving Assertions About Programs, Las Cruces, New Mexico, USA, January 6-7, 1972, pp. 208-211, 1972, ACM, 978-1-4503-7891-8. The full citation details ...](Pics/full.jpeg) |
1972 |
DBLP DOI BibTeX RDF |
|
41 | H. Raymond Strong, S. A. Walker |
Properties preserved under recursion removal. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Proving Assertions About Programs ![In: Proceedings of ACM Conference on Proving Assertions About Programs, Las Cruces, New Mexico, USA, January 6-7, 1972, pp. 97-103, 1972, ACM, 978-1-4503-7891-8. The full citation details ...](Pics/full.jpeg) |
1972 |
DBLP DOI BibTeX RDF |
|
41 | Rod M. Burstall |
An algebraic description of programs with assertions, verification and simulation. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Proving Assertions About Programs ![In: Proceedings of ACM Conference on Proving Assertions About Programs, Las Cruces, New Mexico, USA, January 6-7, 1972, pp. 7-14, 1972, ACM, 978-1-4503-7891-8. The full citation details ...](Pics/full.jpeg) |
1972 |
DBLP DOI BibTeX RDF |
|
39 | David R. Lester |
Real Number Calculations and Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings, pp. 215-229, 2008, Springer, 978-3-540-71065-3. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
Computable Reals, Exact Arithmetic, Theorem Proving, PVS, Higher-order Logic |
37 | Su Feng |
Mechanizing Weakly Ground Termination Proving of Term Rewriting Systems by Structural and Cover-Set Inductions. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Comput. Sci. Technol. ![In: J. Comput. Sci. Technol. 20(4), pp. 496-513, 2005. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
automated formal proving, cover-set induction, dynamic term rewriting calculus, weakly ground termination, term rewriting system |
37 | Wing-Kwong Wong, Bo-Yu Chan, Sheng-Kai Yin |
A Dynamic Geometry Environment for Learning Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICALT ![In: Proceedings of the 5th IEEE International Conference on Advanced Learning Technologies, ICALT 2005, Kaohsiung, Taiwan, July 5-8, 2005, pp. 15-17, 2005, IEEE Computer Society, 0-7695-2338-2. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
learning geometry, geometry education, theorem proving, Dynamic geometry |
37 | Hongbo Li 0012 |
Algebraic Representation, Elimination and Expansion in Automated Geometric Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Automated Deduction in Geometry ![In: Automated Deduction in Geometry, 4th International Workshop, ADG 2002, Hagenberg Castle, Austria, September 4-6, 2002, Revised Papers, pp. 106-123, 2002, Springer, 3-540-20927-1. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
Cayley algebra, bracket algebra, affine geometry, automated theorem proving, projective geometry, conics |
37 | Miroslav Popovic, Vladimir Kovacevic, Ivan Velikic |
A Formal Software Verification Concept Based on Automated Theorem Proving and Reverse Engineering. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ECBS ![In: 9th IEEE International Conference on Engineering of Computer-Based Systems (ECBS 2002), 8-11 April 2002, Lund, Sweden, pp. 59-66, 2002, IEEE Computer Society, 0-7695-1549-5. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
formal software verification, fault-tolerant and robust software, mission-critical embedded software, reverse engineering, automated theorem proving, predicate calculus |
37 | Fausto Giunchiglia, Paolo Traverso |
Theorem proving in technology transfer: the user's point of view. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Int. J. Softw. Tools Technol. Transf. ![In: Int. J. Softw. Tools Technol. Transf. 3(1), pp. 1-12, 2000. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
Formal methods, Mechanized theorem proving |
37 | Mark D. Aagaard, Robert B. Jones, Carl-Johan H. Seger |
Lifted-FL: A Pragmatic Implementation of Combined Model Checking and Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs'99, Nice, France, September, 1999, Proceedings, pp. 323-340, 1999, Springer, 3-540-66463-7. The full citation details ...](Pics/full.jpeg) |
1999 |
DBLP DOI BibTeX RDF |
|
37 | Anna Mikhajlova, Joakim von Wright |
Proving Isomorphism of First-Order Logic Proof Systems in HOL. ![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. 295-314, 1998, Springer, 3-540-64987-5. The full citation details ...](Pics/full.jpeg) |
1998 |
DBLP DOI BibTeX RDF |
|
37 | Sreeranga P. Rajan, Jeffrey J. Joyce, Carl-Johan H. Seger |
From Abstract Data Types to Shift Registers: A Case Study in Formal Specification and Verification at Differing Levels of Abstraction using Theorem Proving and Symbolic Simulation. ![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. 489-500, 1993, Springer, 3-540-57826-9. The full citation details ...](Pics/full.jpeg) |
1993 |
DBLP DOI BibTeX RDF |
|
35 | Benny Godlin, Ofer Strichman |
Inference rules for proving the equivalence of recursive procedures. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Acta Informatica ![In: Acta Informatica 45(6), pp. 403-439, 2008. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
|
35 | Paul A. Cairns, Jeremy Gow |
Literate Proving: Presenting and Documenting Formal Proofs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MKM ![In: Mathematical Knowledge Management, 4th International Conference, MKM 2005, Bremen, Germany, July 15-17, 2005, Revised Selected Papers, pp. 159-173, 2005, Springer, 3-540-31430-X. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
|
35 | Maria Paola Bonacina, Jieh Hsiang |
On Fairness of Completion-Based Theorem Proving Strategies. ![Search on Bibsonomy](Pics/bibsonomy.png) |
RTA ![In: Rewriting Techniques and Applications, 4th International Conference, RTA-91, Como, Italy, April 10-12, 1991, Proceedings, pp. 348-360, 1991, Springer, 3-540-53904-2. The full citation details ...](Pics/full.jpeg) |
1991 |
DBLP DOI BibTeX RDF |
|
35 | Larry Wos |
Solving Open Questions with an Automated Theorem-Proving Program. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: 6th Conference on Automated Deduction, New York, USA, June 7-9, 1982, Proceedings, pp. 1-31, 1982, Springer, 3-540-11558-7. The full citation details ...](Pics/full.jpeg) |
1982 |
DBLP DOI BibTeX RDF |
|
35 | Chih-Hung Wu, Shie-Jue Lee |
On parallelism of hyper-linking theorem proving: a preliminary report. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICPADS ![In: 1996 International Conference on Parallel and Distributed Systems (ICPADS '96), June 3-6, 1996, Tokyo, Japan, Proceedings, pp. 494-499, 1996, IEEE Computer Society, 0-8186-7267-6. The full citation details ...](Pics/full.jpeg) |
1996 |
DBLP DOI BibTeX RDF |
hyper-linking theorem proving, hyper-linking proof procedure, phase-level, clause-level, literal-level, search level parallelism, parallel strategies, parallel algorithms, parallelism, artificial intelligence, parallel architectures, theorem proving |
35 | Miguel Felder, Dino Mandrioli, Angelo Morzenti |
Proving Properties of Real-Time Systems Through Logical Specifications and Petri Net Models. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Trans. Software Eng. ![In: IEEE Trans. Software Eng. 20(2), pp. 127-141, 1994. The full citation details ...](Pics/full.jpeg) |
1994 |
DBLP DOI BibTeX RDF |
property proving, logical specifications, TRIO, Hoare method, dual language, real-time systems, real-time systems, embedded systems, formal specification, formal specification, Petri nets, temporal logic, temporal logic, theorem proving, first-order logic, timed Petri net, formal analysis, axiomatization |
35 | Ming-Yi Fang, Wen-Tsuen Chen |
Vectorization of a Generalized Procedure for Theorem Proving in Propositional Logic on Vector Computers. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Trans. Knowl. Data Eng. ![In: IEEE Trans. Knowl. Data Eng. 4(5), pp. 475-486, 1992. The full citation details ...](Pics/full.jpeg) |
1992 |
DBLP DOI BibTeX RDF |
artificial intelligence, theorem proving, theorem proving, formal logic, propositional logic, vector processor systems, vectorisation, vector computers, deduction rules |
33 | Yingying Jiang 0001, Feng Tian 0001, Hongan Wang, Xiaolong Zhang 0001, XuGang Wang, Guozhong Dai |
Intelligent understanding of handwritten geometry theorem proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IUI ![In: Proceedings of the 15th International Conference on Intelligent User Interfaces, IUI 2010, Hong Kong, China, February 7-10, 2010, pp. 119-128, 2010, ACM, 978-1-60558-515-4. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
geometry theorem proving, hand-drawn figures, hand-written proof scripts, structure based manipulation, recognition |
33 | Hai Lin 0008, Jigui Sun, Yimin Zhang 0005 |
Theorem Proving Based on the Extension Rule. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 31(1), pp. 11-21, 2003. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
extension rule, inclusion-exclusion principle, complementary factor, theorem proving |
33 | Gilles Dowek, Thérèse Hardin, Claude Kirchner |
Theorem Proving Modulo. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 31(1), pp. 33-72, 2003. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
sequent calculus modulo, resolution, rewriting, automated theorem proving, higher-order logic, cut elimination, narrowing, Skolemization, deduction modulo |
33 | Simon J. Gay |
A Framework for the Formalisation of Pi Calculus Type Systems in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 14th International Conference, TPHOLs 2001, Edinburgh, Scotland, UK, September 3-6, 2001, Proceedings, pp. 217-232, 2001, Springer, 3-540-42525-X. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
semantics, Types, pi calculus, automatic theorem proving |
32 | Vlad Rusu, Eli Singerman |
On Proving Safety Properties by Integrating Static Analysis, Theorem Proving and Abstraction. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TACAS ![In: Tools and Algorithms for Construction and Analysis of Systems, 5th International Conference, TACAS '99, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS'99, Amsterdam, The Netherlands, March 22-28, 1999, Proceedings, pp. 178-192, 1999, Springer, 3-540-65703-7. The full citation details ...](Pics/full.jpeg) |
1999 |
DBLP DOI BibTeX RDF |
|
32 | Naren Narasimhan, Ranga Vemuri |
On the Effectiveness of Theorem Proving Guided Discovery of Formal Assertions for a Register Allocator in a High-Level Synthesis System. ![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. 367-386, 1998, Springer, 3-540-64987-5. The full citation details ...](Pics/full.jpeg) |
1998 |
DBLP DOI BibTeX RDF |
|
32 | I. S. W. B. Prasetya |
On the Style of Mechanical Proving. ![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. 475-488, 1993, Springer, 3-540-57826-9. The full citation details ...](Pics/full.jpeg) |
1993 |
DBLP DOI BibTeX RDF |
|
31 | David A. Basin, Hironobu Kuruma, Kunihiko Miyazaki, Kazuo Takaragi, Burkhart Wolff |
Verifying a signature architecture: a comparative case study. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Formal Aspects Comput. ![In: Formal Aspects Comput. 19(1), pp. 63-91, 2007. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
Security, Model checking, Formal methods, Theorem proving, Case study, Comparison |
31 | David A. Plaisted |
Special Cases and Substitutes for Rigid E-Unification. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Appl. Algebra Eng. Commun. Comput. ![In: Appl. Algebra Eng. Commun. Comput. 10(2), pp. 97-152, 2000. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
Rigid E -unification, Theorem proving, First-order logic, Decidability, Unification, Equality, Horn clauses, Tableaux |
31 | Weiqiang Kong, Takahiro Seino, Kokichi Futatsugi, Kazuhiro Ogata 0001 |
A Lightweight Integration of Theorem Proving and Model Checking for System Verification. ![Search on Bibsonomy](Pics/bibsonomy.png) |
APSEC ![In: 12th Asia-Pacific Software Engineering Conference (APSEC 2005), 15-17 December 2005, Taipei, Taiwan, pp. 59-66, 2005, IEEE Computer Society, 0-7695-2465-6. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
|
31 | Christoph Benzmüller, Andreas Meier 0002, Volker Sorge |
Bridging Theorem Proving and Mathematical Knowledge Retrieval. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Mechanizing Mathematical Reasoning ![In: Mechanizing Mathematical Reasoning, Essays in Honor of Jörg H. Siekmann on the Occasion of His 60th Birthday, pp. 277-296, 2005, Springer, 3-540-25051-4. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
|
31 | Helko Lehmann, Michael Leuschel |
Inductive Theorem Proving by Program Specialisation: Generating Proofs for Isabelle Using Ecce. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LOPSTR ![In: Logic Based Program Synthesis and Transformation, 13th International Symposium LOPSTR 2003, Uppsala, Sweden, August 25-27, 2003, Revised Selected Papers, pp. 1-19, 2003, Springer, 3-540-22174-3. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
|
31 | Marta Franová |
Automated Inductive Reasoning as a Support of Deductive Reasoning in a User-Independent Automation of Inductive Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ISMIS ![In: Foundations of Intelligent Systems, 9th International Symposium, ISMIS '96, Zakopane, Poland, June 9-13, 1996, Proceedings, pp. 551-560, 1996, Springer, 3-540-61286-6. The full citation details ...](Pics/full.jpeg) |
1996 |
DBLP DOI BibTeX RDF |
|
31 | Jieh Hsiang, Mandayam K. Srivas |
PROLOG-Based Inductive Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FSTTCS ![In: Foundations of Software Technology and Theoretical Computer Science, Fifth Conference, New Delhi, India, December 16-18, 1985, Proceedings, pp. 129-149, 1985, Springer, 3-540-16042-6. The full citation details ...](Pics/full.jpeg) |
1985 |
DBLP DOI BibTeX RDF |
|
29 | Ueli M. Maurer |
Unifying Zero-Knowledge Proofs of Knowledge. ![Search on Bibsonomy](Pics/bibsonomy.png) |
AFRICACRYPT ![In: Progress in Cryptology - AFRICACRYPT 2009, Second International Conference on Cryptology in Africa, Gammarth, Tunisia, June 21-25, 2009. Proceedings, pp. 272-286, 2009, Springer, 978-3-642-02383-5. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
|
28 | Adel Bouhoula, Jean-Pierre Jouannaud |
Automata-Driven Automated Induction. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LICS ![In: Proceedings, 12th Annual IEEE Symposium on Logic in Computer Science, Warsaw, Poland, June 29 - July 2, 1997, pp. 14-25, 1997, IEEE Computer Society, 0-8186-7925-5. The full citation details ...](Pics/full.jpeg) |
1997 |
DBLP DOI BibTeX RDF |
automata-driven automated induction, inductive theorem proving, first-order functions, finitely many unary membership predicates, rational subsets, ground reducibility, inductive prover, theorem proving, tree automata, Horn Clauses, proof obligations |
28 | Miriam Leeser, John W. O'Leary |
Verification of a subtractive radix-2 square root algorithm and implementation. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICCD ![In: 1995 International Conference on Computer Design (ICCD '95), VLSI in Computers and Processors, October 2-4, 1995, Austin, TX, USA, Proceedings, pp. 526-531, 1995, IEEE Computer Society, 0-8186-7165-3. The full citation details ...](Pics/full.jpeg) |
1995 |
DBLP DOI BibTeX RDF |
subtractive radix-2 square root, floating point square root hardware, Intel Pentium, radix-2 square root, MIPS R4400, RTL level, verification, formal verification, theorem proving, theorem proving, floating point arithmetic, optimizing transformations |
28 | Zohar Manna, Richard J. Waldinger |
Fundamentals of Deductive Program Synthesis. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Trans. Software Eng. ![In: IEEE Trans. Software Eng. 18(8), pp. 674-704, 1992. The full citation details ...](Pics/full.jpeg) |
1992 |
DBLP DOI BibTeX RDF |
deductive program synthesis, deductive-tableau system, theorem-proving framework, nonclausal resolution rule, induction rule, formal specification, artificial intelligence, specification, theorem proving, program testing, reasoning, inference mechanisms, proof |
28 | Robert E. Fields, Morten Elvang-Gøransson |
A VDM Case Study in mural. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Trans. Software Eng. ![In: IEEE Trans. Software Eng. 18(4), pp. 279-295, 1992. The full citation details ...](Pics/full.jpeg) |
1992 |
DBLP DOI BibTeX RDF |
interactive theorem-proving assistant, specification support tool, mural, verification, formal specification, specification, software tools, theorem proving, program verification, interactive systems, VDM, Vienna development method |
28 | Maria Paola Bonacina |
On theorem proving for program checking: historical perspective and recent developments. ![Search on Bibsonomy](Pics/bibsonomy.png) |
PPDP ![In: Proceedings of the 12th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, July 26-28, 2010, Hagenberg, Austria, pp. 1-12, 2010, ACM, 978-1-4503-0132-9. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
combination of theories, rewrite-based theorem proving, speculative inferences, satisfiability modulo theories |
28 | Wolfgang Schreiner |
The RISC ProofNavigator: a proving assistant for program verification in the classroom. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Formal Aspects Comput. ![In: Formal Aspects Comput. 21(3), pp. 277-291, 2009. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
Interactive proving assistants, Teaching formal methods, Computer-aided verification |
28 | Yuyan Chao, Lifeng He, Tsuyoshi Nakamura, Zhenghao Shi, Kenji Suzuki 0001, Hidenori Itoh |
An Improvement of Herbrand's Theorem and Its Application to Model Generation Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Comput. Sci. Technol. ![In: J. Comput. Sci. Technol. 22(4), pp. 541-553, 2007. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
Herbrand’s theorem, Herbrand universe, model generation theorem proving, SATCHMO, really non-propositinal |
28 | Panagiotis Manolios, Daron Vroon 0001 |
Integrating static analysis and general-purpose theorem proving for termination analysis. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICSE ![In: 28th International Conference on Software Engineering (ICSE 2006), Shanghai, China, May 20-28, 2006, pp. 873-876, 2006, ACM, 1-59593-375-1. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
static analysis, theorem proving, termination, liveness, ACL2 |
28 | Chiyan Chen, Hongwei Xi |
Combining programming with theorem proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICFP ![In: Proceedings of the 10th ACM SIGPLAN International Conference on Functional Programming, ICFP 2005, Tallinn, Estonia, September 26-28, 2005, pp. 66-77, 2005, ACM, 1-59593-064-7. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
applied type system, proof erasure, theorem proving, dependent types, ATS |
28 | June Andronick, Boutheina Chetali, Olivier Ly |
Using Coq to Verify Java Card Applet Isolation Properties. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 16th International Conference, TPHOLs 2003, Rom, Italy, September 8-12, 2003, Proceedings, pp. 335-351, 2003, Springer, 3-540-40664-6. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
Security, Theorem Proving, Smart Card |
28 | Stefan Blom, Jaco van de Pol |
State Space Reduction by Proving Confluence. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CAV ![In: Computer Aided Verification, 14th International Conference, CAV 2002,Copenhagen, Denmark, July 27-31, 2002, Proceedings, pp. 596-609, 2002, Springer, 3-540-43997-8. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
on-the-fly state space reduction, symbolic transformation, 7CRL tool set, theorem proving, Labeled transition systems, partial order reduction, confluence, branching bisimulation |
28 | Andrei Voronkov |
How to optimize proof-search in modal logics: new methods of proving redundancy criteria for sequent calculi. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACM Trans. Comput. Log. ![In: ACM Trans. Comput. Log. 2(2), pp. 182-215, 2001. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
theorem proving, modal logic, description logics, proof-search, inverse method |
28 | Harald Ganzinger, Viorica Sofronie-Stokkermans |
Chaining Techniques for Automated Theorem Proving in Many-Valued Logics. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ISMVL ![In: 30th IEEE International Symposium on Multiple-Valued Logic, ISMVL 2000, Portland, Oregon, USA, May 23-25, 2000, Proceedings, pp. 337-344, 2000, IEEE Computer Society, 0-7695-0692-5. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
chaining calculi, resolution, many-valued logic, automated theorem proving, superposition |
28 | Viorica Sofronie-Stokkermans |
Representation Theorems and Theorem Proving in Non-Classical Logics. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ISMVL ![In: 29th IEEE International Symposium on Multiple-Valued Logic, ISMVL 1999, Freiburg im Breisgau, Germany, May 20-22, 1999, Proceedings, pp. 242-247, 1999, IEEE Computer Society, 0-7695-0161-3. The full citation details ...](Pics/full.jpeg) |
1999 |
DBLP DOI BibTeX RDF |
distributive lattices with operators, Priestley duality, many-values logics, automated theorem proving, Non-classical logics |
28 | Oliver Bittel |
Tableau-Based Theorem Proving and Synthesis of Lambda-Terms in the Intuitionistic Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
JELIA ![In: Logics in AI, European Workshop, JELIA '92, Berlin, Germany, September 7-10, 1992, Proceedings, pp. 262-278, 1992, Springer, 3-540-55887-X. The full citation details ...](Pics/full.jpeg) |
1992 |
DBLP DOI BibTeX RDF |
Typed -Calculus, Program Synthesis, Intuitionistic Logic, Automatic Theorem Proving |
28 | Donald I. Good, Richard M. Cohen, James G. Keeton-Williams |
Principles of Proving Programs Correct in Gypsy. ![Search on Bibsonomy](Pics/bibsonomy.png) |
POPL ![In: Conference Record of the Sixth Annual ACM Symposium on Principles of Programming Languages, San Antonio, Texas, USA, January 1979, pp. 42-52, 1979, ACM Press. The full citation details ...](Pics/full.jpeg) |
1979 |
DBLP DOI BibTeX RDF |
message buffers, program proving, formal specifications, parallel programs, concurrency, program verification |
27 | Laurent Théry, Guillaume Hanrot |
Primality Proving with Elliptic Curves. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 20th International Conference, TPHOLs 2007, Kaiserslautern, Germany, September 10-13, 2007, Proceedings, pp. 319-333, 2007, Springer, 978-3-540-74590-7. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
|
27 | Steven Obua |
Proving Bounds for Real Linear Programs in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005, Proceedings, pp. 227-244, 2005, Springer, 3-540-28372-2. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
|
27 | César A. Muñoz, David R. Lester |
Real Number Calculations and Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005, Proceedings, pp. 195-210, 2005, Springer, 3-540-28372-2. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
|
27 | Deepak Kapur, Nikita A. Sakhanenko |
Automatic Generation of Generalization Lemmas for Proving Properties of Tail-Recursive Definitions. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 16th International Conference, TPHOLs 2003, Rom, Italy, September 8-12, 2003, Proceedings, pp. 136-154, 2003, Springer, 3-540-40664-6. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
|
27 | Peter Dybjer, Qiao Haiyan, Makoto Takeyama |
Combining Testing and Proving in Dependent Type Theory. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 16th International Conference, TPHOLs 2003, Rom, Italy, September 8-12, 2003, Proceedings, pp. 188-203, 2003, Springer, 3-540-40664-6. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
|
27 | Konrad Slind, Joe Hurd |
Applications of Polytypism in Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 16th International Conference, TPHOLs 2003, Rom, Italy, September 8-12, 2003, Proceedings, pp. 103-119, 2003, Springer, 3-540-40664-6. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
|
27 | Laurent Théry |
Proving Pearl: Knuth's Algorithm for Prime Numbers. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 16th International Conference, TPHOLs 2003, Rom, Italy, September 8-12, 2003, Proceedings, pp. 304-318, 2003, Springer, 3-540-40664-6. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
|
27 | Klaus Schneider 0001 |
Proving the Equivalence of Microstep and Macrostep Semantics. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 15th International Conference, TPHOLs 2002, Hampton, VA, USA, August 20-23, 2002, Proceedings, pp. 314-331, 2002, Springer, 3-540-44039-9. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
|
27 | Simon Ambler, Roy L. Crole, Alberto Momigliano |
Combining Higher Order Abstract Syntax with Tactical Theorem Proving and (Co)Induction. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 15th International Conference, TPHOLs 2002, Hampton, VA, USA, August 20-23, 2002, Proceedings, pp. 13-30, 2002, Springer, 3-540-44039-9. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
|
27 | Jason Hickey, Aleksey Nogin |
Fast Tactic-Based Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 13th International Conference, TPHOLs 2000, Portland, Oregon, USA, August 14-18, 2000, Proceedings, pp. 252-267, 2000, Springer, 3-540-67863-8. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
|
27 | Roope Kaivola, Mark D. Aagaard |
Divider Circuit Verification with Model Checking and Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 13th International Conference, TPHOLs 2000, Portland, Oregon, USA, August 14-18, 2000, Proceedings, pp. 338-355, 2000, Springer, 3-540-67863-8. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
|
27 | François Puitg, Jean-François Dufourd |
Formal Specification and Theorem Proving Breakthroughs in Geometric Modeling. ![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. 401-422, 1998, Springer, 3-540-64987-5. The full citation details ...](Pics/full.jpeg) |
1998 |
DBLP DOI BibTeX RDF |
|
27 | Flemming Andersen, Kim Dam Petersen, Jimmi S. Pettersson |
A Graphical Tool for Proving Unity Progress. ![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. 17-32, 1994, Springer, 3-540-58450-1. The full citation details ...](Pics/full.jpeg) |
1994 |
DBLP DOI BibTeX RDF |
|
27 | Holger Busch |
First-Order Automation for Higher-Order-Logic Theorem Proving. ![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. 97-112, 1994, Springer, 3-540-58450-1. The full citation details ...](Pics/full.jpeg) |
1994 |
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 |
|
26 | 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 |
26 | Xia Wu, Jigui Sun, Shuai Lu 0001, Ying Li, Wei Meng, Minghao Yin |
Improved Propositional Extension Rule. ![Search on Bibsonomy](Pics/bibsonomy.png) |
RSKT ![In: Rough Sets and Knowledge Technology, First International Conference, RSKT 2006, Chongqing, China, July 24-26, 2006, Proceedings, pp. 592-597, 2006, Springer, 3-540-36297-5. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
Extension rule, reduced rule, theorem proving, propositional logic |
26 | Marcelo Glusman, Shmuel Katz |
A Mechanized Proof Environment for the Convenient Computations Proof Method. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Formal Methods Syst. Des. ![In: Formal Methods Syst. Des. 23(2), pp. 115-142, 2003. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
convenient computations, proof environment, deductive theorem proving, formal verification, PVS |
26 | Herman Geuvers, Gueorgui I. Jojgov |
Open Proofs and Open Terms: A Basis for Interactive Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CSL ![In: Computer Science Logic, 16th International Workshop, CSL 2002, 11th Annual Conference of the EACSL, Edinburgh, Scotland, UK, September 22-25, 2002, Proceedings, pp. 537-552, 2002, Springer, 3-540-44240-5. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
open terms, meta-variables, formulas-as-types, type theory, interactive theorem proving |
26 | Sigrid Gürgens, Javier López 0001 |
Suitability of a Classical Analysis Method for E-commerce Protocols. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ISC ![In: Information Security, 4th International Conference, ISC 2001, Malaga, Spain, October 1-3, 2001, Proceedings, pp. 46-62, 2001, Springer, 3-540-42662-0. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
electronic commerce, cryptographic protocol, Security analysis, automatic theorem proving, protocol validation |
26 | Myla Archer, Constance L. Heitmeyer, Elvinia Riccobene |
Using TAME to prove invariants of automata models: Two case studies. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FMSP ![In: Proceedings of the Third Workshop on Formal Methods in Software Practice, 2000, Portland, Oregon, USA, pp. 25-36, 2000, ACM, 1-58113-262-X. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
software requirements analysis, Software engineering, verification, formal methods, theorem proving |
26 | Mark D. Aagaard, Carl-Johan H. Seger |
The formal verification of a pipelined double-precision IEEE floating-point multiplier. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICCAD ![In: Proceedings of the 1995 IEEE/ACM International Conference on Computer-Aided Design, ICCAD 1995, San Jose, California, USA, November 5-9, 1995, pp. 7-10, 1995, IEEE Computer Society / ACM, 0-8186-7213-7. The full citation details ...](Pics/full.jpeg) |
1995 |
DBLP DOI BibTeX RDF |
ANSI/IEEE Std 754-1985, model checking, theorem proving, floating-point arithmetic, Hardware verification |
26 | Li Dafa |
An Application to Teaching in Logic Course of ATP Based Natural Deduction. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LPAR ![In: Logic Programming and Automated Reasoning,International Conference LPAR'92, St. Petersburg, Russia, July 15-20, 1992, Proceedings, pp. 463-465, 1992, Springer, 3-540-55727-X. The full citation details ...](Pics/full.jpeg) |
1992 |
DBLP DOI BibTeX RDF |
theorem proving, logic, natural deduction |
26 | Li Dafa |
Intelligent CAI Course in the First-Order Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICCAL ![In: Computer Assisted Learning, 3rd International Conference, ICCAL '90, Hagen, FRG, June 11-13, 1990, Proceedings, pp. 67-72, 1990, Springer, 3-540-52699-4. The full citation details ...](Pics/full.jpeg) |
1990 |
DBLP DOI BibTeX RDF |
tautology, theorem proving, first-order logic, resolution, natural deduction |
26 | 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 |
|
26 | Devrim Unal, M. Ufuk Çaglayan |
Theorem proving for modeling and conflict checking of authorization policies. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ISCN ![In: Proceedings of the International Symposium on Computer Networks, ISCN 2006, June 16-18, 2006, Istanbul, Turkey, pp. 146-151, 2006, IEEE. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
|
Displaying result #1 - #100 of 7488 (100 per page; Change: ) Pages: [ 1][ 2][ 3][ 4][ 5][ 6][ 7][ 8][ 9][ 10][ >>] |
|