RDV le pour le 17 juin 2021 pour le GT CLAP aux Journées du GDR GPL! Cette année, nous partagerons notre slot avec le GT HIFI (Méthodes Formelles et Programmation de Systèmes Critiques).
Orateurs:
- Verification of FIFO systems, Etienne Lozes
FIFO systems are systems of automata communicating through FIFO queues. This simple and rather idealised model can be used to analyse some aspects of message-passing systems, reactive systems with event queues, weak memory models with buffered reads and writes, etc. From
a purely computational perspective, this is a Turing complete model even for just one automaton and one FIFO queue.
In this talk, I will present a personal selection of existing works on the problem of the automatic (push-button) verification of such systems. I will consider in particular the works that try to address the verification of FIFO systems that are “nearly” systems with rendez-vous synchronisation.
Nearly synchronous FIFO systems can be found for instance in the work of Lipton on reduction [1], Elrad&Francez on communication closed layers [2],
Bultan et al on synchronisability [3], Mushcoll et al on existential boundedness [4], or more recently Bouajjani et al on k-synchronous systems [5].
This idea is also implicitly present in several works on multi-party session types [6], although the connection there is only well understood in the bipartite setting, where it matches the notion of half-duplex communications [7,8]. The aim of the talk will also be to present recent personal contributions and ongoing works on k-synchronous systems, existentially-bounded systems, and half-duplex systems [9,10,11,12].
[1] Lipton, R.J.: Reduction: A method of proving properties of parallel programs. Commun. ACM 18(12), 717–721 (1975). https://doi.org/10.1145/361227.361234
[2] Elrad, T., Francez, N.: Decomposition of distributed programs into communication-closed layers. Sci. Comput. Program. 2(3), 155–173 (1982). https://doi.org/10.1016/0167-6423(83)90013-8
[3] Basu, S., Bultan, T.: On deciding synchronizability for asynchronously communicating systems. Theor. Comput. Sci. https://doi.org/10.1016/j.tcs.2016.09.023
[4] Genest, B., Kuske, D., Muscholl, A.: On communicating automata with bounded channels. Fundam. Inform. 80(1-3), 147–167 (2007), http://content.iospress.com/articles/fundamenta-informaticae/fi80-1-3-09
[5] Bouajjani, A., Enea, C., Ji, K., Qadeer, S.: On the completeness of verifying message passing programs under bounded asynchrony. CAV’18, https://doi.org/10.1007/978-3-319-96142-2 23, and https://arxiv.org/abs/1804.06612
[6] Honda, K., Yoshida, N., Carbone, M., Multiparty asynchronous session types
https://dl.acm.org/doi/10.1145/1328897.1328472
[7] Cécé, G., Finkel, A. Verification of programs with half-duplex communication. Inf. Comput. 202(2): 166-190 (2005)
https://www.sciencedirect.com/science/article/pii/S0890540105001082?via%3Dihub
[8] Lozes, E., Villard, J. Reliable Contracts for Unreliable Half-Duplex Communications. WS-FM 2011: 2-16
https://link.springer.com/chapter/10.1007%2F978-3-642-29834-9_2
[9] Di Giusto, C., Laversa, L., Lozes, E. On the k-synchronizability of Systems. FoSSaCS 2020: 157-176
https://link.springer.com/chapter/10.1007%2F978-3-030-45231-5_9
[10] Di Giusto, C., Laversa, L., Lozes, E. Guessing the buffer bound for k-synchronizability. CIAA 2021. To appear.
https://arxiv.org/abs/2104.14408
[11] Bollig, B., Di Giusto, C., Finkel, A., Laversa, L., Lozes, E., Suresh, A. A Unifying Framework for Deciding Synchronizability
submitted.
[12] Di Giusto, C., Germerie-Guizouarn, L., Lozes, E., Towards Generalised Half-Duplex Systems.
submitted.
- Sound Semantic Static Analysis for Multiple Languages in the MOPSA Project, Antoine Miné
We present MOPSA, an ongoing project to design a static analyzer by
abstract interpretation targeting multiple languages. Static analyzers
aim at inferring, at compile time, properties of program executions, and
help ensuring their correctness. They perform an interpretation of the
program in an abstract domain of properties that is approximate (to
ensure efficiency) but sound with respect to the semantic of the
language (no false negative). The classic approach to multi-language
analyzers is to use language-specific front-ends to translate programs
into a common, lower-level language (e.g., a subset of C, an
intermediate representation, or a bytecode) before the analysis. The
back-end then iterates over a fixed language using a data abstraction
which is composed of a collection of abstraction modules that can be
plugged in and out to achieve various cost/precision trade-offs.
MOPSA strives to achieve a higher degree of modularity and extensibility
by considering value abstractions, iterators, and control-flow
abstractions uniformly as domain modules. Each module can extend the
language syntax and rewrite expressions and statements to simpler ones
dynamically to be processed by further modules. Hence, we avoid the
pitfalls of fixing a common intermediate representation and we allow the
rewriting to exploit any information found by the analysis so far. We
will present MOPSA’s architecture and some of our applications. These
include a value analysis for C programs that also uses a specification
language for C library functions. We also present type and value
analyses for a significant subset of Python, as well as a value analysis
for Python programs calling native C functions. Despite the variation in
the languages analyzed and the properties inferred, these analyses share
many common abstractions.
- Eric Goubault
Personal musings on semantic models and verification of programs,
hybrid, concurrent and distributed systems »
_Abstract_: In semantics and verification, the end justifies any means.
Applying this old saying to the letter, program and systems modeling and
verification have produced an enormous amount of carefully crafted
mathematics over the last 50 years or so. Being approximately of the
same age, it seemed like a good idea for me to try to describe some of
the methods I have participated in developing, within the Cosynus group
at LIX, based on both numerical and symbolic methods and their interplay.
On the numerical mathematics side, I will describe some of the abstract
interpretation/set-based methods we designed; on the symbolic side of
things, I will pick up a few examples of algebraic (mostly categorical
and higher-categorical), logical (varieties of temporal and epistemic
logics) and geometric (invariants of topological and directed
topological spaces). These are in fact all inter-related when you take
the right categorical perspective, but this may well go too far for a
general presentation.
These mathematics constitute a Swiss Army knife for dealing with a
varieties of applications: checking control systems (for drones and
swarms of drones), possibly including learning-based components (neural
networks for perception and control), solving computability and
complexity problems for diverse models of computation (rewriting
systems, distributed systems etc.) and control and motion planning
algorithms, expressing correctness for concurrent data structures etc.
If time permits, I will direct the audience to some of these
applications whenever possible.
Organisateurs
- Kevin Martin, Université de Bretagne-Sud/Lab-STICC
- Emmanuelle Saillard, Inria
- Frédéric Dabrowski, Université d’Orléans
- Ludovic Henrio, CNRS
- Les responsables du GT HIFI