The HOL-CSP Refinement Toolkit

MaRDI QIDQ7361061FDO

Authors Safouan Taha, Burkhart Wolff, Lina Ye

Publication date 19 November 2020

Cites work

• 9th international conference on automated deduction (CADE-9), Argonne, Illinois, USA, May 23-26, 1988. Proceedings
• Java: Embedding a programming language in a theorem prover
• A formulation of the simple theory of types
• A mechanization of strong Kleene logic for partial functions
• A new application for explanation-based generalisation within automated deduction
• A Theory of Communicating Sequential Processes
• Abstract State Machines
• Advanced software engineering: Expanding the frontiers of software technology. IFIP 19th world computer congress, first international workshop on advanced software engineering, August 25, 2006. Santiago, Chile.
• An introduction to mathematical logic and type theory: To truth through proof.
• Automated deduction -- CADE-11. Proceedings of the 11th international conference held in Saratoga Springs, NY, USA, June 15--18, 1992
• Automated deduction -- CADE-21. 21st international conference on automated deduction, Bremen, Germany, July 17--20, 2007. Proceedings
• Automated reasoning. Third international joint conference, IJCAR 2006, Seattle, WA, USA, August 17--20, 2006. Proceedings
• Automation for interactive proof: first prototype
• Building Formal Method Tools in the Isabelle/Isar Framework
• COLOG-88. International conference on computer logic, Tallinn, USSR, December 12-16, 1988. Proceedings
• Computer aided verification. 8th international conference, CAV '96, New Brunswick, NJ, USA, July 31 -- August 3, 1996. Proceedings
• Computer science logic. 4th workshop, CSL '90, Heidelberg, Germany, October 1--5, 1990. Proceedings
• CoreASM: an extensible ASM execution engine
• Defining liveness
• Demand-Driven Compositional Symbolic Execution
• Dynamic Logic with Non-rigid Functions
• ECOOP '87. European Conference on Object-Oriented Programming, Paris, France, June 15-17, 1987. Proceedings
• ECOOP '98 -- object-oriented programming. 12th European conference, Brussels, Belgium, July 20--24, 1998. Proceedings
• ECOOP 2003 --- object-oriented programming, 17th European conference, Darmstadt, Germany, July 21--25, 2003, Proceedings
• ECOOP 2005 -- object-oriented programming. 19th European conference, Glasgow, UK, July 25--29, 2005. Proceedings
• Efficiently checking propositional refutations in HOL theorem provers
• Error Sensitive Test Cases Analysis (ESTCA)
• EurAsia-ICT 2002: Information and communication technology. First EurAsian conference, Shiraz, Iran, October 29--31, 2002. Proceedings
• FM 2005: Formal Methods
• FM 2005: Formal Methods
• FM 2008: Formal methods. 15th international symposium on formal methods, Turku, Finland, May 26--30, 2008. Proceedings
• FME 2002: Formal methods - getting IT right. International symposium of formal methods Europe, Copenhagen, Denmark, July 22--24, 2002. Proceedings
• Formal Approaches to Software Testing
• Formal approaches to software testing. 4th international workshop, FATES 2004, Linz, Austria, September 21, 2004. Revised selected papers.
• Formal aspects in security and trust. IFIP TC1 WG1.7 workshop on formal aspects in security and trust (FAST), world computer congress, August 22--27, 2004, Toulouse, France.
• Forward and backward simulations. II: Timing-based systems
• Foundations of security analysis and design V. FOSAD 2007/2008/2009 tutorial lectures
• Fuzzy Identity-Based Encryption
• Higher order logic theorem proving and its applications. 6th International Workshop, HUG '93, Vancouver, B. C., Canada, August 11-13, 1993. Proceedings
• HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier
• HOLCF = HOL + LCF
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Integrating a SAT solver with an LCF-style theorem prover
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Introduction to mathematical philosophy. 1. Auflage 1919, 2. Auflage 1920.
• Isabelle/HOL. A proof assistant for higher-order logic
• LCF-Style Propositional Simplification with BDDs and SAT Solvers
• lean\(T^ AP\): Lean tableau-based deduction
• Literate Programming
• Logical frameworks
• Many-Valued Logic, Partiality, and Abstraction in Formal Specification Languages
• Natural deduction for non-classical logics
• Notions of computation and monads
• Object modeling with the OCL. The rationale behind the object constraint language
• Obvious inferences
• On Hoare logic and Kleene algebra with tests
• On message specifications in OCL
• Operating system verification---an overview
• Path Feasibility Analysis for String-Manipulating Programs
• Perspectives of system informatics. 4th international Andrei Ershov memorial conference, PSI 2001, Akademgorodok, Novosibirsk, Russia, July 2--6, 2001. Revised papers
• Philosophers May Dine - Definitively!
• Privacy-Aware Attribute-Based Encryption with User Accountability
• Protection in operating systems
• Proving and applying program transformations expressed with second-order patterns
• Proving the Correctness of Multiprocess Programs
• Refinement and retrenchment for programming language data types
• SDL 2001: meeting UML. 10th international SDL forum, Copenhagen, Denmark, June 27--29, 2001. Proceedings
• Semantic essence of AsmL
• Source-Level Proof Reconstruction for Interactive Theorem Proving
• Specification of object-oriented systems
• System Description: Spass Version 3.0
• Tableaux for many-valued logics
• Testing can be formal, too
• Testing of software and communicating systems. 19th IFIP TC6/WG6.1 international conference, TestCom 2007, 7th international workshop, FATES 2007, Tallinn, Estonia, June 26--29, 2007. Proceedings
• Testing of software and communication systems. 21st IFIP WG 6.1 international conference, TESTCOM 2009 and 9th international workshop, FATES 2009, Eindhoven, The Netherlands, November 2--4, 2009. Proceedings
• Tests and proofs. Second international conference, TAP 2008, Prato, Italy, April 9--11, 2008. Proceedings
• The B-Book
• The Mathematics of the Pentium Division Bug
• The Open-Source Fixed-Point Model Checker for Symbolic Analysis of Security Protocols
• Theorem Proving in Higher Order Logics
• Theorem Proving in Higher Order Logics
• Theorem proving in higher order logics. 18th international conference, TPHOLs 2005, Oxford, UK, August 22--25, 2005. Proceedings.
• Theorem proving in higher order logics. 20th international conference, TPHOLs 2007, Kaiserslautern, Germany, September 10--13, 2007. Proceedings
• Theorem proving in higher order logics. 21st international conference, TPHOLs 2008, Montreal, Canada, August 18--21, 2008. Proceedings
• Theoretical aspects of computing -- ICTAC 2005. Second international colloquium, Hanoi, Vietnam, October 17--21, 2005. Proceedings
• Theoretical Aspects of Computing – ICTAC 2005
• Tools and Algorithms for the Construction and Analysis of Systems
• Tools and algorithms for the construction and analysis of systems. 12th international conference, TACAS 2006, held as part of the joint European conferences on theory and practice of software, ETAPS 2006, Vienna, Austria, March 25 -- April 2, 2006. Procee
• Tools and algorithms for the construction and analysis of systems. 14th international conference, TACAS 2008, held as part of the joint European conferences on theory and practice of software, ETAPS 2008, Budapest, Hungary, March 29--April 6, 2008. Procee
• Tools and algorithms for the construction and analysis of systems. 15th international conference, TACAS 2009, held as part of the joint European conferences on theory and practice of software, ETAPS 2009, York, UK, March 22--29, 2009. Proceedings
• Tools and algorithms for the construction and analysis of systems. 7th international conference, TACAS 2001, held as part of the joint European conferences on theory and practice of software, ETAPS 2001, Genova, Italy, April 2--6, 2001. Proceedings
• Translating higher-order clauses to first-order clauses
• VDM '88. VDM (Vienna development method) - The way ahead. 2nd VDM-Europe symposium, Dublin, Ireland, September 11-16, 1988. Proceedings
• Winskel is (almost) right: Towards a mechanized semantics textbook

This page was built for software: The HOL-CSP Refinement Toolkit