Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
15 | Björn Pelzer, Christoph Wernhard |
System Description: E-KRHyper. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-21, 21st International Conference on Automated Deduction, Bremen, Germany, July 17-20, 2007, Proceedings, pp. 508-513, 2007, Springer, 978-3-540-73594-6. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
|
15 | Todd Deshane, Wenjin Hu, Patty Jablonski, Hai Lin 0005, Christopher Lynch, Ralph Eric McGregor |
Encoding First Order Proofs in SAT. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-21, 21st International Conference on Automated Deduction, Bremen, Germany, July 17-20, 2007, Proceedings, pp. 476-491, 2007, Springer, 978-3-540-73594-6. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
|
15 | Achim D. Brucker, Burkhart Wolff |
Test-Sequence Generation with Hol-TestGen with an Application to Firewall Testing. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TAP ![In: Tests and Proofs - 1st International Conference, TAP 2007, Zurich, Switzerland, February 12-13, 2007. Revised Papers, pp. 149-168, 2007, Springer, 978-3-540-73769-8. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
symbolic test case generations, theorem proving, computer security, black box testing, Isabelle/HOL, test sequence generation |
15 | Osman Hasan, Sofiène Tahar |
Verification of Probabilistic Properties in HOL Using the Cumulative Distribution Function. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IFM ![In: Integrated Formal Methods, 6th International Conference, IFM 2007, Oxford, UK, July 2-5, 2007, Proceedings, pp. 333-352, 2007, Springer, 978-3-540-73209-9. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
Higher-Order-Logic, Interactive Theorem Proving, HOL, Probabilistic Systems, Cumulative Distribution Function |
15 | José Luis Freire-Nistal, Enrique Freire Brañas, Antonio Blanco Ferro, David Cabrero Souto |
On the Representation of Imperative Programs in a Logical Framework. ![Search on Bibsonomy](Pics/bibsonomy.png) |
EUROCAST ![In: Computer Aided Systems Theory - EUROCAST 2007, 11th International Conference on Computer Aided Systems Theory, Las Palmas de Gran Canaria, Spain, February 12-16, 2007, Revised Selected Papers, pp. 202-209, 2007, Springer, 978-3-540-75866-2. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
|
15 | J Strother Moore |
Inductive assertions and operational semantics. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Int. J. Softw. Tools Technol. Transf. ![In: Int. J. Softw. Tools Technol. Transf. 8(4-5), pp. 359-371, 2006. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
Theorem proving, JVM, Software verification, Verification condition |
15 | J. Christian Attiogbé |
Multi-process Systems Analysis Using Event B: Application to Group Communication Systems. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICFEM ![In: Formal Methods and Software Engineering, 8th International Conference on Formal Engineering Methods, ICFEM 2006, Macao, China, November 1-3, 2006, Proceedings, pp. 660-677, 2006, Springer, 3-540-47460-9. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
Event B, Dynamic Architecture, Group Communication Systems, Property verification |
15 | Jim Woodcock 0001, Leo Freitas |
Z/Eves and the Mondex Electronic Purse. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICTAC ![In: Theoretical Aspects of Computing - ICTAC 2006, Third International Colloquium, Tunis, Tunisia, November 20-24, 2006, Proceedings, pp. 15-34, 2006, Springer, 3-540-48815-4. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
electronic finance, software archaeology, the Z notation, Z/Eves, security, refinement, theorem proving, smart cards, Grand Challenge, Verified Software Repository, Mondex |
15 | Viktor Kuncak, Martin C. Rinard |
An overview of the Jahob analysis system: project goals and current status. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IPDPS ![In: 20th International Parallel and Distributed Processing Symposium (IPDPS 2006), Proceedings, 25-29 April 2006, Rhodes Island, Greece, 2006, IEEE. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
|
15 | Thomas Tuerk, Klaus Schneider 0001, Mike Gordon |
Model Checking PSL Using HOL and SMV. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Haifa Verification Conference ![In: Hardware and Software, Verification and Testing, Second International Haifa Verification Conference, HVC 2006, Haifa, Israel, October 23-26, 2006. Revised Selected Papers, pp. 1-15, 2006, Springer, 978-3-540-70888-9. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
|
15 | Li Ye, Junliang Chen |
Automatic Composition of Semantic Web Services - A Theorem Proof Approach. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ASWC ![In: The Semantic Web - ASWC 2006, First Asian Semantic Web Conference, Beijing, China, September 3-7, 2006, Proceedings, pp. 481-487, 2006, Springer, 3-540-38329-8. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
Automatic Theorem Proof, Deductive Program Synthesis, Semantic Web Services, Automatic Service Composition |
15 | Andrei Voronkov |
Inconsistencies in Ontologies. ![Search on Bibsonomy](Pics/bibsonomy.png) |
JELIA ![In: Logics in Artificial Intelligence, 10th European Conference, JELIA 2006, Liverpool, UK, September 13-15, 2006, Proceedings, pp. 19, 2006, Springer, 3-540-39625-X. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
|
15 | 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 |
15 | Pedro Quaresma, Predrag Janicic |
Integrating Dynamic Geometry Software, Deduction Systems, and Theorem Repositories. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MKM ![In: Mathematical Knowledge Management, 5th International Conference, MKM 2006, Wokingham, UK, August 11-12, 2006, Proceedings, pp. 280-294, 2006, Springer, 3-540-37104-4. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
|
15 | Steve Roach, Jeffrey Van Baalen |
Automated Procedure Construction for Deductive Synthesis. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Autom. Softw. Eng. ![In: Autom. Softw. Eng. 12(4), pp. 393-414, 2005. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
synthesis, procedures, deductive, decision, partial deduction |
15 | John Harrison 0001 |
A HOL Theory of Euclidean Space. ![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. 114-129, 2005, Springer, 3-540-28372-2. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
|
15 | Jim Woodcock 0001, Ana Cavalcanti 0001, Leonardo Freitas |
Operational Semantics for Model Checking Circus. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FM ![In: FM 2005: Formal Methods, International Symposium of Formal Methods Europe, Newcastle, UK, July 18-22, 2005, Proceedings, pp. 237-252, 2005, Springer, 3-540-27882-6. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
|
15 | K. Rustan M. Leino, Francesco Logozzo |
Loop Invariants on Demand. ![Search on Bibsonomy](Pics/bibsonomy.png) |
APLAS ![In: Programming Languages and Systems, Third Asian Symposium, APLAS 2005, Tsukuba, Japan, November 2-5, 2005, Proceedings, pp. 119-134, 2005, Springer, 3-540-29735-9. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
|
15 | Oliver Ray |
The Need for Ancestor Resolution When Answering Queries in Horn Clause Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICLP ![In: Logic Programming, 21st International Conference, ICLP 2005, Sitges, Spain, October 2-5, 2005, Proceedings, pp. 410-411, 2005, Springer, 3-540-29208-X. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
|
15 | Chad E. Brown |
Reasoning in Extensional Type Theory with Equality. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-20, 20th International Conference on Automated Deduction, Tallinn, Estonia, July 22-27, 2005, Proceedings, pp. 23-37, 2005, Springer, 3-540-28005-7. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
|
15 | Ittai Balaban, Amir Pnueli, Lenore D. Zuck |
Shape Analysis by Predicate Abstraction. ![Search on Bibsonomy](Pics/bibsonomy.png) |
VMCAI ![In: Verification, Model Checking, and Abstract Interpretation, 6th International Conference, VMCAI 2005, Paris, France, January 17-19, 2005, Proceedings, pp. 164-180, 2005, Springer, 3-540-24297-X. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
|
15 | Yannick Chevalier, Laurent Vigneron |
Strategy for Verifying Security Protocols with Unbounded Message Size. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Autom. Softw. Eng. ![In: Autom. Softw. Eng. 11(2), pp. 141-166, 2004. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
intruder model, automatic strategies, verification, security protocols, flaw detection |
15 | Toh Ne Win, Michael D. Ernst, Stephen J. Garland, Dilsun Kirli Kaynar, Nancy A. Lynch |
Using simulated execution in verifying distributed algorithms. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Int. J. Softw. Tools Technol. Transf. ![In: Int. J. Softw. Tools Technol. Transf. 6(1), pp. 67-76, 2004. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
Invariant detection, Static analysis, Theorem proving, Dynamic analysis |
15 | Alexander Koller, Ralph Debusmann, Malte Gabsdil, Kristina Striegnitz |
Put My Galakmid Coin into the Dispenser and Kick It: Computational Linguistics and Theorem Proving in a Computer Game. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Log. Lang. Inf. ![In: J. Log. Lang. Inf. 13(2), pp. 187-206, 2004. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
text adventures, generation, description logic, parsing, theorem provers, reference resolution, dependency grammar |
15 | Daniel Winterstein, Alan Bundy, Corin A. Gurr, Mateja Jamnik |
An Experimental Comparison of Diagrammatic and Algebraic Logics. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Diagrams ![In: Diagrammatic Representation and Inference, Third International Conference, Diagrams 2004, Cambridge, UK, March 22-24, 2004, Proceedings, pp. 432-434, 2004, Springer, 3-540-21268-X. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
15 | Jerzy Marcinkowski, Jan Otop, Grzegorz Stelmaszek |
On a Semantic Subsumption Test. ![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. 142-153, 2004, Springer, 3-540-25236-3. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
15 | Sandip Ray, Warren A. Hunt Jr. |
Deductive Verification of Pipelined Machines Using First-Order Quantification. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CAV ![In: Computer Aided Verification, 16th International Conference, CAV 2004, Boston, MA, USA, July 13-17, 2004, Proceedings, pp. 31-43, 2004, Springer, 3-540-22342-8. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
15 | Alexander Krupp, Wolfgang Müller 0003, Ian Oliver |
Formal Refinement and Model Checking of an Echo Cancellation Unit. ![Search on Bibsonomy](Pics/bibsonomy.png) |
DATE ![In: 2004 Design, Automation and Test in Europe Conference and Exposition (DATE 2004), 16-20 February 2004, Paris, France, pp. 102-107, 2004, IEEE Computer Society, 0-7695-2085-5. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
15 | Yue Tang, Jin Song Dong, Jing Sun 0002, Brendan P. Mahony |
Reasoning about Semantic Web in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
APSEC ![In: 11th Asia-Pacific Software Engineering Conference (APSEC 2004), 30 November - 3 December 2004, Busan, Korea, pp. 46-53, 2004, IEEE Computer Society, 0-7695-2245-9. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
15 | Jinghai Rao, Peep Küngas, Mihhail Matskin |
Logic-based Web Services Composition: From Service Description to Process Model. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICWS ![In: Proceedings of the IEEE International Conference on Web Services (ICWS'04), June 6-9, 2004, San Diego, California, USA, pp. 446-453, 2004, IEEE Computer Society, 0-7695-2167-3. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
15 | Terrance Swift |
Deduction in Ontologies via ASP. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LPNMR ![In: Logic Programming and Nonmonotonic Reasoning, 7th International Conference, LPNMR 2004, Fort Lauderdale, FL, USA, January 6-8, 2004, Proceedings, pp. 275-288, 2004, Springer, 3-540-20721-X. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
15 | Simon Colton, Andreas Meier 0002, Volker Sorge, Roy L. McCasland |
Automatic Generation of Classification Theorems for Finite Algebras. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IJCAR ![In: Automated Reasoning - Second International Joint Conference, IJCAR 2004, Cork, Ireland, July 4-8, 2004, Proceedings, pp. 400-414, 2004, Springer, 3-540-22345-2. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
15 | Tjark Weber |
Towards Mechanized Program Verification with Separation Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CSL ![In: Computer Science Logic, 18th International Workshop, CSL 2004, 13th Annual Conference of the EACSL, Karpacz, Poland, September 20-24, 2004, Proceedings, pp. 250-264, 2004, Springer, 3-540-23024-6. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
Separation Logic, Interactive Theorem Proving, Formal Program Verification |
15 | Juan Carlos López Pimentel, Raúl Monroy |
A Rippling-Based Difference Reduction Technique to Automatically Prove Security Protocol Goals. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IBERAMIA ![In: Advances in Artificial Intelligence - IBERAMIA 2004, 9th Ibero-American Conference on AI, Puebla, Mexico, November 22-26, 2004, Proceedings, pp. 364-374, 2004, Springer, 3-540-23806-9. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
15 | Sandeep S. Kulkarni, Borzoo Bonakdarpour, Ali Ebnenasir |
Mechanical Verification of Automatic Synthesis of Fault-Tolerant Programs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LOPSTR ![In: Logic Based Program Synthesis and Transformation, 14th International Symposium, LOPSTR 2004, Verona, Italy, August 26-28, 2004, Revised Selected Papers, pp. 36-52, 2004, Springer, 3-540-26655-0. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
Addition of faulttolerance, Fault-tolerance, Program transformation, Theorem proving, Program synthesis, PVS, Mechanical verification |
15 | Diana Toma, Dominique Borrione, Ghiath Al Sammane |
Combining Several Paradigms for Circuit Validation and Verification. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CASSIS ![In: Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, International Workshop, CASSIS 2004, Marseille, France, March 10-14, 2004, Revised Selected Papers, pp. 229-249, 2004, Springer, 3-540-24287-2. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
15 | Fairouz Kamareddine, Manuel Maarek, J. B. Wells |
Flexible Encoding of Mathematics on the Computer. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MKM ![In: Mathematical Knowledge Management, Third International Conference, MKM 2004, Bialowieza, Poland, September 19-21, 2004, Proceedings, pp. 160-174, 2004, Springer, 3-540-23029-7. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
15 | Claudio Sacerdoti Coen |
Mathematical Libraries as Proof Assistant Environments. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MKM ![In: Mathematical Knowledge Management, Third International Conference, MKM 2004, Bialowieza, Poland, September 19-21, 2004, Proceedings, pp. 332-346, 2004, Springer, 3-540-23029-7. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
15 | Lars-Åke Fredlund, Dilian Gurov, Thomas Noll 0001, Mads Dam, Thomas Arts, Gennady Chugunov |
A verification tool for ERLANG. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Int. J. Softw. Tools Technol. Transf. ![In: Int. J. Softw. Tools Technol. Transf. 4(4), pp. 405-420, 2003. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
Formal methods, Theorem proving, Software verification |
15 | Jens Busch, Wolfgang Banzhaf |
How to Program Artificial Chemistries. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ECAL ![In: Advances in Artificial Life, 7th European Conference, ECAL 2003, Dortmund, Germany, September 14-17, 2003, Proceedings, pp. 20-30, 2003, Springer, 3-540-20057-6. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
|
15 | Marcelo F. Frias, Carlos López Pombo, Gabriel Baum, Nazareno Aguirre, T. S. E. Maibaum |
Taking Alloy to the Movies. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FME ![In: FME 2003: Formal Methods, International Symposium of Formal Methods Europe, Pisa, Italy, September 8-14, 2003, Proceedings, pp. 678-697, 2003, Springer, 3-540-40828-2. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
|
15 | Francisco-Jesús Martín-Mateos, José-Antonio Alonso, María-José Hidalgo, José-Luis Ruiz-Reina |
Formal Verification of Molecular Computational Models in ACL2: A Case Study. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CAEPIA ![In: Current Topics in Artificial Intelligence, 10th Conference of the Spanish Association for Artificial Intelligence, CAEPIA 2003, and 5th Conference on Technology Transfer, TTIA 2003, San Sebastian, Spain, November 12-14, 2003. Revised Selected Papers, pp. 344-353, 2003, Springer, 3-540-22218-9. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
|
15 | Warren A. Hunt Jr., Robert Bellarmine Krug, J Strother Moore |
Linear and Nonlinear Arithmetic in ACL2. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CHARME ![In: Correct Hardware Design and Verification Methods, 12th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2003, L'Aquila, Italy, October 21-24, 2003, Proceedings, pp. 319-333, 2003, Springer, 3-540-20363-X. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
|
15 | 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 |
15 | Jinghai Rao, Xiaomeng Su |
Toward the Composition of Semantic Web Services. ![Search on Bibsonomy](Pics/bibsonomy.png) |
GCC (2) ![In: Grid and Cooperative Computing, Second International Workshop, GCC 2003, Shanghai, China, December 7-10, 2003, Revised Papers, Part II, pp. 760-767, 2003, Springer, 3-540-21993-5. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
|
15 | 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 |
15 | Aleksey Nogin, Jason Hickey |
Sequent Schema for Derived Rules. ![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. 281-297, 2002, Springer, 3-540-44039-9. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
|
15 | Michael W. Whalen, Johann Schumann, Bernd Fischer 0002 |
Synthesizing Certified Code. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FME ![In: FME 2002: Formal Methods - Getting IT Right, International Symposium of Formal Methods Europe, Copenhagen, Denmark, July 22-24, 2002, Proceedings, pp. 431-450, 2002, Springer, 3-540-43928-5. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
automatic program synthesis, code certification, program verification, automated theorem proving, proof-carrying code |
15 | Michael Backes 0001, Christian Jacobi 0002, Birgit Pfitzmann |
Deriving Cryptographically Sound Implementations Using Composition and Formally Verified Bisimulation. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FME ![In: FME 2002: Formal Methods - Getting IT Right, International Symposium of Formal Methods Europe, Copenhagen, Denmark, July 22-24, 2002, Proceedings, pp. 310-329, 2002, Springer, 3-540-43928-5. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
security, cryptography, formal verification, PVS, simulatability |
15 | Ashish Tiwari 0001, Gaurav Khanna 0001 |
Series of Abstractions for Hybrid Automata. ![Search on Bibsonomy](Pics/bibsonomy.png) |
HSCC ![In: Hybrid Systems: Computation and Control, 5th International Workshop, HSCC 2002, Stanford, CA, USA, March 25-27, 2002, Proceedings, pp. 465-478, 2002, Springer, 3-540-43321-X. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
|
15 | Luís Cruz-Filipe |
A Constructive Formalization of the Fundamental Theorem of Calculus. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: Types for Proofs and Programs, Second International Workshop, TYPES 2002, Berg en Dal, The Netherlands, April 24-28, 2002, Selected Papers, pp. 108-126, 2002, Springer, 3-540-14031-X. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
|
15 | Hans de Nivelle |
Extraction of Proofs from the Clausal Normal Form Transformation. ![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. 584-598, 2002, Springer, 3-540-44240-5. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
|
15 | Marianne Brown |
Selecting Semantics for Use with Semantic Pruning of Linear Deductions. ![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. 719, 2002, Springer, 3-540-00197-2. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
|
15 | Jeremy E. Dawson, Rajeev Goré |
Machine-Checking the Timed Interval Calculus. ![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. 95-106, 2002, Springer, 3-540-00197-2. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
Reasoning about time, theorem proving, automated reasoning |
15 | Christoph Kern, Tarik Ono-Tesfaye, Mark R. Greenstreet |
A light-weight framework for hardware verification. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Int. J. Softw. Tools Technol. Transf. ![In: Int. J. Softw. Tools Technol. Transf. 3(3), pp. 286-313, 2001. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
Refinement, Theorem-proving, Timing verification, Switch-level models, SRT division |
15 | Giampaolo Bella, Lawrence C. Paulson |
Mechanical Proofs about a Non-repudiation Protocol. ![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. 91-104, 2001, Springer, 3-540-42525-X. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
|
15 | Klaus Schneider 0001 |
Embedding Imperative Synchronous Languages in Interactive Theorem Provers. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACSD ![In: 2nd International Conference on Application of Concurrency to System Design (ACSD 2001), 25-30 June 2001, Newcastle upon Tyne, UK, pp. 143-, 2001, IEEE Computer Society, 0-7695-1071-X. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
|
15 | Uwe Waldmann |
Superposition and Chaining for Totally Ordered Divisible Abelian Groups. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IJCAR ![In: Automated Reasoning, First International Joint Conference, IJCAR 2001, Siena, Italy, June 18-23, 2001, Proceedings, pp. 226-241, 2001, Springer, 3-540-42254-4. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
|
15 | Andrea Formisano 0001, Eugenio G. Omodeo, Marco Temperini |
Instructing Equational Set-Reasoning with Otter. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IJCAR ![In: Automated Reasoning, First International Joint Conference, IJCAR 2001, Siena, Italy, June 18-23, 2001, Proceedings, pp. 152-167, 2001, Springer, 3-540-42254-4. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
Set reasoning, map algebra, first-order theorem proving |
15 | 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 |
|
15 | Jens Schönherr, Bernd Straube |
Automatic Equivalence Check of Circuit Descriptions at Clocked Algorithmic and Register Transfer Level. ![Search on Bibsonomy](Pics/bibsonomy.png) |
DATE ![In: 2000 Design, Automation and Test in Europe (DATE 2000), 27-30 March 2000, Paris, France, pp. 759, 2000, IEEE Computer Society / ACM, 0-7695-0537-6. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
|
15 | Marianne Brown, Geoff Sutcliffe |
System Description: PTTP+GLiDes: Semantically Guided PTTP. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-17, 17th International Conference on Automated Deduction, Pittsburgh, PA, USA, June 17-20, 2000, Proceedings, pp. 411-416, 2000, Springer, 3-540-67664-3. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
|
15 | Alexandre Riazanov, Andrei Voronkov |
Partially Adaptive Code Trees. ![Search on Bibsonomy](Pics/bibsonomy.png) |
JELIA ![In: Logics in Artificial Intelligence, European Workshop, JELIA 2000 Malaga, Spain, September 29 - October 2, 2000, Proceedings, pp. 209-223, 2000, Springer, 3-540-41131-3. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
term indexing, code trees, matching, automated theorem proving, subsumption |
15 | Florian Kammüller, Markus Wenzel 0001, Lawrence C. Paulson |
Locales - A Sectioning Concept for Isabelle. ![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. 149-166, 1999, Springer, 3-540-66463-7. The full citation details ...](Pics/full.jpeg) |
1999 |
DBLP DOI BibTeX RDF |
|
15 | Nazanin Mansouri, Ranga Vemuri |
Accounting for Various Register Allocation Schemes During Post-Synthesis Verification of RTL Designs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
DATE ![In: 1999 Design, Automation and Test in Europe (DATE '99), 9-12 March 1999, Munich, Germany, pp. 223-, 1999, IEEE Computer Society / ACM, 0-7695-0078-1. The full citation details ...](Pics/full.jpeg) |
1999 |
DBLP DOI BibTeX RDF |
|
15 | Xiaoping Jia, Sushant Sawant, Jiangyu Zhou, Sotiris Skevoulis |
Detecting Null Pointer Violations in Java Programs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
COMPSAC ![In: 23rd International Computer Software and Applications Conference (COMPSAC '99), 27-19 October 1999, Phoenix, AZ, USA, pp. 456-461, 1999, IEEE Computer Society, 0-7695-0368-3. The full citation details ...](Pics/full.jpeg) |
1999 |
DBLP DOI BibTeX RDF |
|
15 | Jacques D. Fleuriot, Lawrence C. Paulson |
Proving Newton's Propositio Kepleriana Using Geometry and Nonstandard Analysis in Isabelle. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Automated Deduction in Geometry ![In: Automated Deduction in Geometry, Second International Workshop, ADG'98, Beijing, China, August 1-3, 1998, Proceedings, pp. 47-66, 1998, Springer, 3-540-66672-9. The full citation details ...](Pics/full.jpeg) |
1998 |
DBLP DOI BibTeX RDF |
|
15 | Matthew Wilding |
A Machine-Checked Proof of the Optimality of a Real-Time Scheduling Policy. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CAV ![In: Computer Aided Verification, 10th International Conference, CAV '98, Vancouver, BC, Canada, June 28 - July 2, 1998, Proceedings, pp. 369-378, 1998, Springer, 3-540-64608-6. The full citation details ...](Pics/full.jpeg) |
1998 |
DBLP DOI BibTeX RDF |
|
15 | David A. Plaisted, Yunshan Zhu |
Replacement Rules with Definition Detection. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FTP (LNCS Selection) ![In: Automated Deduction in Classical and Non-Classical Logics, Selected Papers, pp. 80-94, 1998, Springer, 3-540-67190-0. The full citation details ...](Pics/full.jpeg) |
1998 |
DBLP DOI BibTeX RDF |
|
15 | Hajime Sawamura, Daisaku Asanuma |
Mechanizing Relevant Logics with 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. 443-460, 1998, Springer, 3-540-64987-5. The full citation details ...](Pics/full.jpeg) |
1998 |
DBLP DOI BibTeX RDF |
|
15 | Florian Kammüller |
Modular Structures as Dependent Types in Isabelle. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: Types for Proofs and Programs, International Workshop TYPES '98, Kloster Irsee, Germany, March 27-31, 1998, Selected Papers, pp. 121-132, 1998, Springer, 3-540-66537-4. The full citation details ...](Pics/full.jpeg) |
1998 |
DBLP DOI BibTeX RDF |
|
15 | Jacques D. Fleuriot, Lawrence C. Paulson |
A Combination of Nonstandard Analysis and Geometry Theorem Proving, with Application to Newton's Principia. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-15, 15th International Conference on Automated Deduction, Lindau, Germany, July 5-10, 1998, Proceedings, pp. 3-16, 1998, Springer, 3-540-64675-2. The full citation details ...](Pics/full.jpeg) |
1998 |
DBLP DOI BibTeX RDF |
|
15 | Carsten Schürmann, Frank Pfenning |
Automated Theorem Proving in a Simple Meta-Logic for LF. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-15, 15th International Conference on Automated Deduction, Lindau, Germany, July 5-10, 1998, Proceedings, pp. 286-300, 1998, Springer, 3-540-64675-2. The full citation details ...](Pics/full.jpeg) |
1998 |
DBLP DOI BibTeX RDF |
|
15 | Andreas Wolf |
p-SETHEO: Strategy Parallelism in Automated Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TABLEAUX ![In: Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX '98, Oisterwijk, The Netherlands, May 5-8, 1998, Proceedings, pp. 320-324, 1998, Springer, 3-540-64406-7. The full citation details ...](Pics/full.jpeg) |
1998 |
DBLP DOI BibTeX RDF |
|
15 | Andreas Wolf |
Strategy Selection for Automated Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
AIMSA ![In: Artificial Intelligence: Methodology, Systems, and Applications, 8th International Conference, AIMSA '98, Sozopol, Bulgaria, September 21-13, 1998, Proceedings, pp. 452-465, 1998, Springer, 3-540-64993-X. The full citation details ...](Pics/full.jpeg) |
1998 |
DBLP DOI BibTeX RDF |
|
15 | Martin Simons 0001 |
Proof Presentation for Isabelle. ![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. 259-274, 1997, Springer, 3-540-63379-0. The full citation details ...](Pics/full.jpeg) |
1997 |
DBLP DOI BibTeX RDF |
|
15 | Sten Agerholm, Jacob Frost |
Towards an Integrated CASE and Theorem Proving Tool for VDM-SL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FME ![In: FME '97: Industrial Applications and Strengthened Foundations of Formal Methods, 4th International Symposium of Formal Methods Europe, Graz, Austria, September 15-19, 1997, Proceedings, pp. 278-297, 1997, Springer, 3-540-63533-5. The full citation details ...](Pics/full.jpeg) |
1997 |
DBLP DOI BibTeX RDF |
|
15 | Bernd Fischer 0002, Johann Schumann |
SETHEO Goes Software Engineering: Application of ATP to Software Reuse. ![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. 65-68, 1997, Springer, 3-540-63104-6. The full citation details ...](Pics/full.jpeg) |
1997 |
DBLP DOI BibTeX RDF |
|
15 | Susanne Graf, Hassen Saïdi |
Verifying Invariants Using theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CAV ![In: Computer Aided Verification, 8th International Conference, CAV '96, New Brunswick, NJ, USA, July 31 - August 3, 1996, Proceedings, pp. 196-207, 1996, Springer, 3-540-61474-5. The full citation details ...](Pics/full.jpeg) |
1996 |
DBLP DOI BibTeX RDF |
|
15 | Edmund M. Clarke, Steven M. German, Xudong Zhao 0005 |
Verifying the SRT Division Algorithm Using Theorem Proving Techniques. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CAV ![In: Computer Aided Verification, 8th International Conference, CAV '96, New Brunswick, NJ, USA, July 31 - August 3, 1996, Proceedings, pp. 111-122, 1996, Springer, 3-540-61474-5. The full citation details ...](Pics/full.jpeg) |
1996 |
DBLP DOI BibTeX RDF |
|
15 | Leopoldo E. Bertossi, Javier Pinto, Pablo Sáez, Deepak Kapur, Mahadevan Subramaniam |
Automating Proofs of Integrity Constraints in Situation Calculus. ![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. 212-222, 1996, Springer, 3-540-61286-6. The full citation details ...](Pics/full.jpeg) |
1996 |
DBLP DOI BibTeX RDF |
|
15 | Tanel Tammet, Jan M. Smith |
Optimized Encodings of Fragments of Type Theory in First Order Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: Types for Proofs and Programs, International Workshop TYPES'95, Torino, Italy, June 5-8, 1995, Selected Papers, pp. 265-287, 1995, Springer, 3-540-61780-9. The full citation details ...](Pics/full.jpeg) |
1995 |
DBLP DOI BibTeX RDF |
|
15 | 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 |
|
15 | I. S. W. B. Prasetya |
Towards a Mechanically Supported and Compositional Calculus to Design Destributed Algorithms. ![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. 362-377, 1994, Springer, 3-540-58450-1. The full citation details ...](Pics/full.jpeg) |
1994 |
DBLP DOI BibTeX RDF |
|
15 | Laurent Vigneron |
Associative-Commutative Deduction with Constraints. ![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. 530-544, 1994, Springer, 3-540-58156-1. The full citation details ...](Pics/full.jpeg) |
1994 |
DBLP DOI BibTeX RDF |
|
15 | Mark E. Stickel, Richard J. Waldinger, Michael R. Lowry, Thomas Pressburger, Ian Underwood |
Deductive Composition of Astronomical Software from Subroutine Libraries. ![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. 341-355, 1994, Springer, 3-540-58156-1. The full citation details ...](Pics/full.jpeg) |
1994 |
DBLP DOI BibTeX RDF |
|
15 | Manfred Broy, Ursula Hinkel, Tobias Nipkow, Christian Prehofer, Birgit Schieder |
Interpreter Verification for a Functional Language. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FSTTCS ![In: Foundations of Software Technology and Theoretical Computer Science, 14th Conference, Madras, India, December 15-17, 1994, Proceedings, pp. 77-88, 1994, Springer, 3-540-58715-2. The full citation details ...](Pics/full.jpeg) |
1994 |
DBLP DOI BibTeX RDF |
|
15 | Deepak Kapur, Mahadevan Subramaniam |
Using Linear Arithmetic Procedure for Generating Induction Schemes. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FSTTCS ![In: Foundations of Software Technology and Theoretical Computer Science, 14th Conference, Madras, India, December 15-17, 1994, Proceedings, pp. 438-449, 1994, Springer, 3-540-58715-2. The full citation details ...](Pics/full.jpeg) |
1994 |
DBLP DOI BibTeX RDF |
|
15 | Reiner Hähnle, Werner Kernig |
Verification of Switch-Level Designs with Many-Valued Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LPAR ![In: Logic Programming and Automated Reasoning,4th International Conference, LPAR'93, St. Petersburg, Russia, July 13-20, 1993, Proceedings, pp. 158-169, 1993, Springer, 3-540-56944-8. The full citation details ...](Pics/full.jpeg) |
1993 |
DBLP DOI BibTeX RDF |
|
15 | John Harrison 0001, Laurent Théry |
Reasoning About the Reals: The Marriage of HOL and Maple. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LPAR ![In: Logic Programming and Automated Reasoning,4th International Conference, LPAR'93, St. Petersburg, Russia, July 13-20, 1993, Proceedings, pp. 351-353, 1993, Springer, 3-540-56944-8. The full citation details ...](Pics/full.jpeg) |
1993 |
DBLP DOI BibTeX RDF |
|
15 | Hardi Hungar |
Combining Model Checking and Theorem Proving to Verify Parallel Processes. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CAV ![In: Computer Aided Verification, 5th International Conference, CAV '93, Elounda, Greece, June 28 - July 1, 1993, Proceedings, pp. 154-165, 1993, Springer, 3-540-56922-7. The full citation details ...](Pics/full.jpeg) |
1993 |
DBLP DOI BibTeX RDF |
|
15 | Robert P. Kurshan, Leslie Lamport |
Verification of a Multiplier: 64 Bits and Beyond. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CAV ![In: Computer Aided Verification, 5th International Conference, CAV '93, Elounda, Greece, June 28 - July 1, 1993, Proceedings, pp. 166-179, 1993, Springer, 3-540-56922-7. The full citation details ...](Pics/full.jpeg) |
1993 |
DBLP DOI BibTeX RDF |
|
15 | I. S. W. B. Prasetya |
Formalization of Variables Access Constraints to Support Compositionality of Liveness Properties. ![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. 324-337, 1993, Springer, 3-540-57826-9. The full citation details ...](Pics/full.jpeg) |
1993 |
DBLP DOI BibTeX RDF |
|
15 | Ricardo Caferra, Michel Herment |
GLEFATINF: A Graphic Framework for Combining Theorem Provers and Editing Proofs for Different Logics. ![Search on Bibsonomy](Pics/bibsonomy.png) |
DISCO ![In: Design and Implementation of Symbolic Computation Systems, International Symposium, DISCO '93, Gmunden, Austria, September 15-17, 1993, Proceedings, pp. 229-240, 1993, Springer, 3-540-57235-X. The full citation details ...](Pics/full.jpeg) |
1993 |
DBLP DOI BibTeX RDF |
Graphic Proof Presentation, Proof Edition, Logical Frameworks |
15 | Dominique Borrione, Laurence V. Pierre, Ashraf M. Salem |
Formal Verification of VHDL Descriptions in the Prevail Environment. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Des. Test Comput. ![In: IEEE Des. Test Comput. 9(2), pp. 42-56, 1992. The full citation details ...](Pics/full.jpeg) |
1992 |
DBLP DOI BibTeX RDF |
|
15 | Geoffrey D. Alexander, David A. Plaisted |
Proving Equality Theorems with Hyper-Linking. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-11, 11th International Conference on Automated Deduction, Saratoga Springs, NY, USA, June 15-18, 1992, Proceedings, pp. 706-710, 1992, Springer, 3-540-55602-8. The full citation details ...](Pics/full.jpeg) |
1992 |
DBLP DOI BibTeX RDF |
|
15 | David A. Randell, Anthony G. Cohn 0001, Zhan Cui |
Computing Transivity Tables: A Challenge For Automated Theorem Provers. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-11, 11th International Conference on Automated Deduction, Saratoga Springs, NY, USA, June 15-18, 1992, Proceedings, pp. 786-790, 1992, Springer, 3-540-55602-8. The full citation details ...](Pics/full.jpeg) |
1992 |
DBLP DOI BibTeX RDF |
|
15 | Dave Barker-Plummer, Sidney C. Bailin, Andrew S. Merrill |
&: Automated Natural Deduction. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-11, 11th International Conference on Automated Deduction, Saratoga Springs, NY, USA, June 15-18, 1992, Proceedings, pp. 716-720, 1992, Springer, 3-540-55602-8. The full citation details ...](Pics/full.jpeg) |
1992 |
DBLP DOI BibTeX RDF |
|
15 | Paul Loewenstein, David L. Dill |
Verification of a Multiprocessor Cache Protocol Using Simulation Relations and Higher-Order Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CAV ![In: Computer Aided Verification, 2nd International Workshop, CAV '90, New Brunswick, NJ, USA, June 18-21, 1990, Proceedings, pp. 302-311, 1990, Springer, 3-540-54477-1. The full citation details ...](Pics/full.jpeg) |
1990 |
DBLP DOI BibTeX RDF |
|
15 | Amy P. Felty, Dale Miller 0001 |
Encoding a Dependent-Type Lambda-Calculus in a Logic Programming Language. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: 10th International Conference on Automated Deduction, Kaiserslautern, FRG, July 24-27, 1990, Proceedings, pp. 221-235, 1990, Springer, 3-540-52885-7. The full citation details ...](Pics/full.jpeg) |
1990 |
DBLP DOI BibTeX RDF |
|