Generation of Executable Code for Isabelle/HOL-CSP Models
Level: L3/M1/M2
Contact: B. Wolff, A. Durier
Description
The theory of Communicating Sequential Processes (CSP) going back to Hoare and Roscoe [2] is still today one of the reference theories for concurrent specification and computing. This theory has been presented in Isabelle/HOL based on the denotational semantics of the Failure/Divergence Model of CSP. In particular, the resulting theory project HOL-CSP [1] can cope with infinite alphabets, in contrast to model-checking approaches that are limited to finite ones. The theories also comprise a derived operational semantics of the entire language [3].
The purpose of this work is to use code-generation techniques of the Isabelle system in order to generat procedures that generate concrete random runs out of HOL-CSP models. The core idea is to evolve configurations (F,P) (where F is a constraint set and P a process term) to configurations (F',P') by applying a rule of the operational semantics
P ~e~> P'
where e is an admissible event. Typically, the randomly chosen e must also be consistent/a partial solution of F. The overall goal is to construct random-traces up to a given depth with possibilities to inspect the resulting final process state.
Workplan
- Understanding the existing library and constructing a work-setup inside Isabelle
- Implementing the new core functionality
- Developing a Suite of smaller examples for testing
Required Skills
- functional programming skills
- interest in compiler construction
- knowledge in concurrency and programming semantics desirable
- interest in automated constraint solving (inside Isabelle)
Bibliography
[1] HOL-CSP 2.0: The GIT for the Isabelle/HOL-CSP project. Git - Link.
[2] A.W. Roscoe. Theory and Practice of Concurrency. Prentice Hall, 1997.
[3] B. Ballenghien, B. Wolff: An Operational Semantics in Isabelle/HOL-CSP. ITP 2024, LIPIcs 309, 7:1-7:18
[4] Thomas Genet, Joergen Villadsen : Isabelle: An introduction.
[5] Isabelle/HOL and the Isabelle Archive of Formal Methods: Overview and General AFP Entry and Isabelle on Wikipedia.
[6] Makarius Wenzel, Burkhart Wolff: Building Formal Method Tools in the Isabelle/Isar Framework. TPHOLs 2007: 352-367
[7] Labelled Transition System. Labelled Transition Systems. And: slides.
[8] Benoit Ballenghien, Tianwen Gu et Burkhart Wolff: Certifying FDR4 Checks by HOL-CSP Proofs. Submitted.
An Isabelle/DOF Ontology for Mathematical Libraries in the AFP
Contact: B. Wolff, I. Ait-Sadoune
The linking of formal and informal information is perhaps the most pervasive challenge in the digitization of modern society. Extracting knowledge from reasonably well-structured “raw”-texts is a crucial prerequisite for any form of advanced search, classification, “semantic” validation and “semantic” merge technology. This challenge incites numerous research efforts summarized under the labels “semantic web” or “data mining”. A key role in structuring this linking is played by ontologies (also called “vocabulary” in semantic web communities), i.e., a machine-readable form of the structure of documents and the document discourse.
In this internship, we are interested in ontologies for the growing body of formalised mathematics in Lean or Isabelle, in particular in mathematical libraries such as the Lean Mathlib as well as the Isabelle AFP.
For example, the OntoMathPRO ontology~[1] is an OWL ontology of mathematical knowledge concepts. It possesses the is-a semantics for hierarchies of mathematical knowledge elements, and defines these elements as two hierarchies of classes: a taxonomy of the fields of mathematics and a taxonomy of mathematical knowledge objects. It defines two main type of relations for these two taxonomies: directed relations between elements of the two hierarchies like belongs_to, contains, defines, is_defined_by, solves, is_solved_by, and a symmetric transitive associative relation see_also between two mathematical knowledge objects. It also represents links with external resources such as DBpedia [2].
Isabelle/HOL [3] is a well-known semi-automated proof environment and documentation generator. Isabelle’s Document Ontology Framework (Isabelle/DOF) [4] is an extension of the former. Isabelle/DOF is a new kind of ontological modelling and document validation tool. In contrast to conventional languages like OWL and development environments such as Protége, it extends the Isabelle/HOL core by a number of constructs, allowing for the specification of formal ontologies; additionally, it provides documentation constructs for text-, definition-, term-, proof-, code-, and user-defined elements that enforce document conformance to a given ontology.
In this internship, ideas from OntoMathPRO can be used/adapted to develop a genuine and practically useable Isabelle/DOF ontology for Mathematics. The goal is to generate annotations for major parts of the Isabelle/AFP (LLM technology might be used for this part of the task). A simple search technology for concepts in the annotated Math-sources in Scala should be developed.
Workplan
- Understanding the existing library and constructing a work-setup inside Isabelle
- Implementing an Isabelle/DOF ontology
- Developing an annotated AFP version using meta-data generated from the latter
- Combining search-facilities in Isabelle/Scala to a small query language
- Developing a suite of search examples for testing.
Required Skills
- functional programming skills
- interest in compiler construction
- knowledge in Ontological Modelling desirable,
- General knowledge about various fields in mathematics (Ideal for an LDD3 Math Info or similar)
Bibliography
[1] Olga Nevzorova, Nikita Zhiltsov, Alexander Kirillovich, Evgeny Lipachev: OntoMathPRO Ontology: A Linked Data Hub for Mathematics. ArchivX 2014.
[2] Soren Auer, Christian Bizer, Georgi Kobilarov, Jens Lehmann, Richard Cyganiak, and Zachary Ives: DBpedia: A Nucleus for a Web of Open Data. ISWC/ASWC 2007, LNCS 4825, pp. 722–735, 2007.
[3] Isabelle/HOL and the Isabelle Archive of Formal Methods: Overview and General AFP Entry and Isabelle on Wikipedia.
[4] Achim D. Brucker, Idir Aït-Sadoune, Nicolas Méric, and Burkhart Wolff: Parametric Ontologies in formal Software Engineering. In: Science of Computer Programming. DOI: 10.1016/J.SCICO.2024.103231. Volume 241, Jan 2025.
An LTS Library with Functions for Test-Generation
Level: L3
Contact: B. Wolff (wolff@lmf.cnrs.fr)
Description
Labelled Transition Systems (LTS) [4,5] are a Graph-like data-structure consisting of Nodes and Transitions that may be labelled with additional information. They were used to denote, for example, control-flow-graphs (CFG’s), data-flow-graphs (DFGs), game theory, abstractions of operational executions, and in particular concurrent executions.
The aim for this stage is to enlarge an existing library of LTS’s in SML running inside the Isabelle system. Particular emphasis is put on bi-simulation algorithms, i.e. concrete procedures establishing trace-inclusions on automata, and algorithms implementing coverage criteria known from testing such as “allStates”, “allTransitions” and “allPath(k)”. Developing first proof support for this ki nd of generated formulas can be addressed in a later stage of this internship.
This project stands in the context of the Isabelle/HOL-CSP/FDR project [3,5,6], implemented in Isabelle/HOL[1,2], which links a theory on concurrency with the FDR4 model-checker. By this tool-chain, it is possible to generate for a model of a concurrent system in CSP and the conceptual Programming language IMP_CSP the corresponding LTS’s in the above-mentioned library and to produce Test-traces from these models.
Workplan
- Understanding the existing library and constructing a work-setup inside Isabelle
- Implementing the new core functionality
- Developing a Suite of smaller examples for testing
Required Skills
- functional programming skills
- interest in compiler construction
- knowledge in concurrency and programming semantics desirable, but not necessary
Bibliography
[1] Thomas Genet, Joergen Villadsen : Isabelle: An introduction.
[2] Isabelle/HOL and the Isabelle Archive of Formal Methods: Overview and General AFP Entry and Isabelle on Wikipedia.
[3] Makarius Wenzel, Burkhart Wolff: Building Formal Method Tools in the Isabelle/Isar Framework. TPHOLs 2007: 352-367
[4] Labelled Transition System. Labelled Transition Systems. And: slides.
[5] Benoit Ballenghien, Tianwen Gu et Burkhart Wolff: Certifying FDR4 Checks by HOL-CSP Proofs. Submitted.
[6] HOL-CSP 2.0: The GIT for the Isabelle/HOL-CSP project. Git - Link.
[7] A.W. Roscoe. Theory and Practice of Concurrency. Prentice Hall, 1997.
[8] A.W. Roscoe. Understanding Concurrent Systems. Springer-Verlag, Berlin, Heidelberg, 1st edition, 2010.
A HOL-CSP Case-Study : Analysing the Plain-Old-Telephone Protocol
Contact: B. Wolff, A. Durier, Benoit Ballenghien
Description
The theory of Communicating Sequential Processes going back to Hoare and Roscoe is still today one of the reference theories for concurrent specification and computing. This theory has been presented in Isabelle/HOL based on the denotational semantics of the Failure/Divergence Model of CSP ... The "Plain Old Telephone Service" is a standard medium-size example for architectural modeling of a concurrent system ...
The goal of this stage is a formal analysis of deadlock- and life lock properties of this protocol via interactive proof in Isabelle/HOL.
Connecting Isabelle/C with Isabelle/AutoCorres
Level: M1 / M2
Contact: B. Wolff
Isabelle/C is a framework for C code in C11 syntax deeply integrated into the Isabelle/PIDE development environment. Our framework provides an abstract interface for verification back-ends to be plugged-in independently. The purpose of this stage is to develop a translation from C11-AST's generated in Isabelle/C to a semantic backend called AutoCorres, a complex execution model of the C ;language executed on ARM processors.
This ambitious project is actually a re-implementation and integration of existing prototypes: there is actually a Isabelle/C/AutoCorres version based on Isabelle2021 which is functional enough to serve as reference. However, AutoCorres exists meanwhile as a much more recent and self-contained AFP submission (see here), and the technologies inside Isabelle/C to compile the C11-AST's to a semantic backend have also dramatically improved. Since the long-term goal is a submission of Isabelle/C together with the AutoCorres backend, a re-implementation is necessary.