| 1. |
- Armstrong, Alasdair, et al.
(author)
-
Kleene Algebra
- 2013
-
In: Archive of Formal Proofs. - 2150-914X.
-
Journal article (peer-reviewed)
|
|
| 2. |
- Armstrong, Alasdair, et al.
(author)
-
Program Analysis and Verification Based on Kleene Algebra in Isabelle/HOL
- 2013
-
In: Interactive Theorem Proving. - Berlin, Heidelberg : Springer Berlin/Heidelberg. - 9783642396335 ; , s. 197-212
-
Conference paper (peer-reviewed)abstract
- Schematic Kleene algebra with tests (SKAT) supports the equational verification of flowchart scheme equivalence and captures simple while-programs with assignment statements. We formalise SKAT in Isabelle/HOL, using the quotient type package to reason equationally in this algebra. We apply this formalisation to a complex flowchart transformation proof from the literature. We extend SKAT with assertion statements and derive the inference rules of Hoare logic. We apply this extension in simple program verification examples and the derivation of additional Hoare-style rules. This shows that algebra can provide an abstract semantic layer from which different program analysis and verification tasks can be implemented in a simple lightweight way.
|
|
| 3. |
- Armstrong, Alasdair, et al.
(author)
-
Programming and automating mathematics in the Tarski-Kleene hierarchy
- 2014
-
In: Journal of Logical and Algebraic Methods in Programming. - : Elsevier BV. - 2352-2208. ; 83:2, s. 87-102
-
Journal article (peer-reviewed)abstract
- We present examples from a reference implementation of variants of Kleene algebras and Tarski's relation algebras in the theorem proving environment Isabelle/HOL. For Kleene algebras we show how models can be programmed, including sets of traces and paths, languages, binary relations, max-plus and min-plus algebras, matrices, formal power series. For relation algebras we discuss primarily proof automation in a comprehensive library and present an advanced formalisation example.
|
|
| 4. |
- Bartocci, Ezio, et al.
(author)
-
TOOLympics 2019 : An overview of competitions in formal methods
- 2019
-
In: Tools and Algorithms for the Construction and Analysis of Systems. - Cham : Springer. - 9783030175016 ; , s. 3-24
-
Conference paper (peer-reviewed)abstract
- Evaluation of scientific contributions can be done in many different ways. For the various research communities working on the verification of systems (software, hardware, or the underlying involved mechanisms), it is important to bring together the community and to compare the state of the art, in order to identify progress of and new challenges in the research area. Competitions are a suitable way to do that.The first verification competition was created in 1992 (SAT competition), shortly followed by the CASC competition in 1996. Since the year 2000, the number of dedicated verification competitions is steadily increasing. Many of these events now happen regularly, gathering researchers that would like to understand how well their research prototypes work in practice. Scientific results have to be reproducible, and powerful computers are becoming cheaper and cheaper, thus, these competitions are becoming an important means for advancing research in verification technology.TOOLympics 2019 is an event to celebrate the achievements of the various competitions, and to understand their commonalities and differences. This volume is dedicated to the presentation of the 16 competitions that joined TOOLympics as part of the celebration of the 25?ℎ anniversary of the TACAS conference.
|
|
| 5. |
- Bengtson, Jesper, et al.
(author)
-
Psi-Calculi in Isabelle
- 2016
-
In: Journal of automated reasoning. - : Springer Science and Business Media LLC. - 0168-7433 .- 1573-0670. ; 56:1, s. 1-47
-
Journal article (peer-reviewed)abstract
- This paper presents a mechanisation of psi-calculi, a parametric framework for modelling various dialects of process calculi including (but not limited to) the pi-calculus, the applied pi-calculus, and the spi calculus. psi-calculi are significantly more expressive, yet their semantics is as simple in structure as the semantics of the original pi-calculus. Proofs of meta-theoretic properties for psi-calculi are more involved, however, not least because psi-calculi (unlike simpler calculi) utilise binders that bind multiple names at once. The mechanisation is carried out in the Nominal Isabelle framework, an interactive proof assistant designed to facilitate formal reasoning about calculi with binders. Our main contributions are twofold. First, we have developed techniques that allow efficient reasoning about calculi that bind multiple names in Nominal Isabelle. Second, we have adopted these techniques to mechanise substantial results from the meta-theory of psi-calculi, including congruence properties of bisimilarity and the laws of structural congruence. To our knowledge, this is the most extensive formalisation of process calculi mechanised in a proof assistant to date.
|
|
| 6. |
- Cok, David R., et al.
(author)
-
The 2013 Evaluation of SMT-COMP and SMT-LIB
- 2015
-
In: Journal of automated reasoning. - : Springer Science and Business Media LLC. - 0168-7433 .- 1573-0670. ; 55:1, s. 61-90
-
Journal article (peer-reviewed)abstract
- After 8 years of SMT Competitions, the SMT Steering Committee decided, for 2013, to sponsor an evaluation of the status of SMT benchmarks and solvers, rather than another competition. This report summarizes the results of the evaluation, conducted by the authors. The key observations are that (1) the competition results are quite sensitive to randomness and (2) the most significant need for the future is assessment and improvement of benchmarks in the light of SMT applications. The evaluation also measured competitiveness of solvers, general coverage of solvers, logics, and benchmarks, and degree of repeatability of measurements and competitions.
|
|
| 7. |
- Cok, David R., et al.
(author)
-
The 2013 SMT Evaluation
- 2014
-
Reports (other academic/artistic)abstract
- After 8 years of SMT Competitions, the SMT Steering Committee decided, for 2013, to sponsor an evaluation of the status of SMT benchmarks and solvers, rather than another competition. This report summarizes the results of the evaluation, conducted by the authors. The key observations are that (1) the competition results are quite sensitive to randomness and (2) the most significant need for the future is assessment and improvement of benchmarks in the light of SMT applications. The evaluation also measured competitiveness of solvers, general coverage of solvers, logics, and benchmarks, and degree of repeatability of measurements and competitions.
|
|
| 8. |
- Gengelbach, Arve
(author)
-
Conservative Definitions for Higher-order Logic with Ad-hoc Overloading
- 2021
-
Doctoral thesis (other academic/artistic)abstract
- With an ever growing dependency on computer systems, the need to guarantee their correct behaviour increases. Mathematically rigorous techniques like formal verification offer a way to derive a system's mathematical properties for example with the help of a theorem prover. A theorem prover is a type of software that assists a user in deriving theorems expressed in a formal language. With a theorem prover one should never be able to prove something that is contradictory, as otherwise the proof effort is worthless. This property is called consistency and is essential for formal developments.Theorem provers enjoy high confidence, since they often rely on a trusted logical kernel that is enriched with new symbols in a controlled way. Instead of asserting the existence of mathematical objects with their desired properties, new symbols are introduced through definitions. These definitions are checked by this kernel, and expected to act as abbreviations. Any theorem that is expressible without a definition should not need that definition in its proof. A definition satisfying this property is called conservative. Conservative definitions are especially important as they preserve consistency, so that a proof of a contradiction is not possible after adding these definitions.Isabelle/HOL is a prominent theorem prover with the unique feature of permitting different definitions of one constant at non-overlapping types. In addition to these so-called overloading definitions, a symbol may be used before it is defined. These features mean that consistency or conservativity arguments for simpler logics do not immediately apply to Isabelle/HOL. In the past, design flaws in the definitional mechanism made theories in the Isabelle/HOL theorem prover inconsistent, e.g. it was possible to derive a contradiction from cyclic definitions.With this thesis we show that (overloading) definitions in higher-order logic (HOL) are conservative, hence not source of inconsistency. We define and prove a notion of conservativity that applies to theories of overloading definitions in higher-order logic and formalise aspects of our results in a theorem prover. As a practical implication, when searching for a proof of a formula, our syntactic conservativity criterion allows to exclude irrelevant symbols. In particular, our results confirm that Isabelle/HOL theories are consistent, thus users cannot introduce contradictions through definitions. As a specialisation of our work, our notion of conservativity holds for variants of HOL without overloading. Overall, our work contributes to the understanding of higher-order logic with overloading definitions.
|
|
| 9. |
- Gengelbach, Arve, et al.
(author)
-
Mechanisation of Model-theoretic Conservative Extension for HOL with Ad-hoc Overloading
- 2021
-
In: Proceedings Fifteenth Workshop on Logical Frameworks and Meta-Languages. - : Open Publishing Association. ; , s. 1-17
-
Conference paper (peer-reviewed)abstract
- Definitions of new symbols merely abbreviate expressions in logical frameworks, and no new facts (regarding previously defined symbols) should hold because of a new definition. In Isabelle/HOL, definable symbols are types and constants. The latter may be ad-hoc overloaded, i.e. have different definitions for non-overlapping types. We prove that symbols that are independent of a new definition may keep their interpretation in a model extension. This work revises our earlier notion of model-theoretic conservative extension and generalises an earlier model construction. We obtain consistency of theories of definitions in higher-order logic (HOL) with ad-hoc overloading as a corollary. Our results are mechanised in the HOL4 theorem prover.
|
|
| 10. |
- Gengelbach, Arve, et al.
(author)
-
Model-theoretic Conservative Extension of Definitional Theories
- 2018
-
In: Electronic Notes in Theoretical Computer Science. - : Elsevier BV. - 1571-0661. ; 338, s. 133-145
-
Journal article (peer-reviewed)abstract
- Many logical frameworks allow extensions, i.e. the introduction of new symbols, by definitions. Different from asserting arbitrary non-logical axioms, extensions by definitions are expected to be conservative: they should entail no new theorems in the original language. The popular theorem prover Isabelle implements a variant of higher-order logic that allows ad hoc overloading of constants. In 2015, Kunčar and Popescu introduced definitional theories, which impose a non-circularity condition on constant and type definitions in this logic, and showed that this condition is sufficient for definitional extensions to preserve consistency. We strengthen and generalize this result by showing that extensions of definitional theories are model-theoretic conservative, i.e. every model of the original theory can be expanded to a model of the extended theory.
|
|
| 11. |
- Gengelbach, Arve, et al.
(author)
-
Proof-theoretic Conservativity for HOL with Ad-hoc Overloading
- 2020
-
In: Theoretical Aspects of Computing - ICTAC 2020 - 17th International Colloquium, Macau, China, November 30 - December 4, 2020. - Cham : Springer. - 9783030642761 ; , s. 23-42
-
Conference paper (peer-reviewed)abstract
- Logical frameworks are often equipped with an extensional mechanism to define new symbols. The definitional mechanism is expected to be conservative, i.e. it shall not introduce new theorems of the original language. The theorem proving framework Isabelle implements a variant of higher-order logic where constants may be ad-hoc overloaded, allowing a constant to have different definitions for non-overlapping types. In this paper we prove soundness and completeness for the logic of Isabelle/HOL with general (Henkin-style) semantics, and we prove model-theoretic and proof-theoretic conservativity for theories of definitions.
|
|
| 12. |
- Gomes, Victor B. F., et al.
(author)
-
Kleene Algebras with Domain
- 2016
-
In: Archive of Formal Proofs. - 2150-914X.
-
Journal article (peer-reviewed)
|
|
| 13. |
- Parrow, Joachim, et al.
(author)
-
Modal Logics for Nominal Transition Systems
- 2015
-
In: 26th International Conference on Concurrency Theory. - Dagstuhl, Germany : Leibniz-Zentrum für Informatik. - 9783939897910 ; , s. 198-211
-
Conference paper (peer-reviewed)
|
|
| 14. |
- Parrow, Joachim, et al.
(author)
-
Modal Logics for Nominal Transition Systems
- 2021
-
In: Logical Methods in Computer Science. - 1860-5974. ; 17:1
-
Journal article (peer-reviewed)abstract
- We define a general notion of transition system where states and action labels can be from arbitrary nominal sets, actions may bind names, and state predicates from an arbitrary logic define properties of states. A Hennessy-Milner logic for these systems is introduced, and proved adequate and expressively complete for bisimulation equivalence. A main technical novelty is the use of finitely supported infinite conjunctions. We show how to treat different bisimulation variants such as early, late, open and weak in a systematic way, explore the folklore theorem that state predicates can be replaced by actions, and make substantial comparisons with related work. The main definitions and theorems have been formalised in Nominal Isabelle.
|
|
| 15. |
- Parrow, Joachim, et al.
(author)
-
Modal Logics for Nominal Transition Systems
- 2015
-
Reports (other academic/artistic)abstract
- We define a uniform semantic substrate for a wide variety of process calculi where states and action labels can be from arbitrary nominal sets. A Hennessy-Milner logic for these systems is introduced, and proved adequate for bisimulation equivalence. A main novelty is the use of finitely supported infinite conjunctions. We show how to treat different bisimulation variants such as early, late and open in a systematic way, and make substantial comparisons with related work. The main definitions and theorems have been formalized in Nominal Isabelle.
|
|
| 16. |
- Parrow, Joachim, et al.
(author)
-
The largest respectful function
- 2016
-
In: Logical Methods in Computer Science. - 1860-5974. ; 12:2
-
Journal article (peer-reviewed)abstract
- Respectful functions were introduced by Sangiorgi as a compositional tool to formulate short and clear bisimulation proofs. Usually, the larger the respectful function, the easier the bisimulation proof. In particular the largest respectful function, defined as the pointwise union of all respectful functions, has been shown to be very useful. We here provide an explicit and constructive characterization of it.
|
|
| 17. |
- Parrow, Joachim, et al.
(author)
-
Weak Nominal Modal Logic
- 2017
-
In: Formal Techniques for Distributed Objects, Components, and Systems. - Cham : Springer. - 9783319602240 ; , s. 179-193
-
Conference paper (peer-reviewed)
|
|
| 18. |
|
|
| 19. |
|
|
| 20. |
- Torstensson, Olle, et al.
(author)
-
Hammering Floating-Point Arithmetic
- 2023
-
In: FRONTIERS OF COMBINING SYSTEMS, FROCOS 2023. - Cham : Springer. - 9783031433689 - 9783031433696 ; , s. 217-235
-
Conference paper (peer-reviewed)abstract
- Sledgehammer, a component of the interactive proof assistant Isabelle/HOL, aims to increase proof automation by automatically discharging proof goals with the help of external provers. Among these provers are a group of satisfiability modulo theories (SMT) solvers with support for the SMT-LIB input language. Despite existing formalizations of IEEE floating-point arithmetic in both Isabelle/HOL and SMT-LIB, Sledgehammer employs an abstract translation of floating-point types and constants, depriving the SMT solvers of the opportunity to make use of their dedicated decision procedures for floating-point arithmetic.We show that, by extending Sledgehammer’s translation from the language of Isabelle/HOL into SMT-LIB with an interpretation of floating-point types and constants, floating-point reasoning in SMT solvers can be made available to Isabelle/HOL. Our main contribution is a description and implementation of such an extension. An evaluation of the extended translation shows a significant increase of Sledgehammer’s success rate on proof goals involving floating-point arithmetic.
|
|
| 21. |
|
|
| 22. |
|
|
| 23. |
- Weber, Tjark, et al.
(author)
-
The 2014 SMT Competition
- 2016
-
In: Journal on Satisfiability, Boolean Modeling and Computation. - 1875-5011 .- 1574-0617.
-
Journal article (peer-reviewed)
|
|
