Étienne Renault

In International Journal on Software Tools for Technology Transfer (STTT)

Abstract We introduce Go2Pins, a tool that takes a program written in Go and links it with two model-checkers: LTSMin and Spot. Go2Pins is an effort to promote the integration of both formal verification and testing inside industrial-size projects. With this goal in mind, we introduce black-box transitions, an efficient and scalable technique for handling the Go runtime. This approach, inspired by hardware verification techniques, allows easy, automatic and efficient abstractions.

Towards better heuristics for solving bounded model checking problems

By Anissa Kheireddine, Étienne Renault, Souheib Baarir

2022-12-09

In Constraints

Abstract This paper presents a new way to improve the performance of the SAT-based bounded model checking problem on sequential and parallel procedures by exploiting relevant information identified through the characteristics of the original problem. This led us to design a new way of building interesting heuristics based on the structure of the underlying problem. The proposed methodology is generic and can be applied for any SAT problem. This paper compares the state-of-the-art approaches with two new heuristics for sequential procedures: Structure-based and Linear Programming heuristics.

Tuning SAT solvers for LTL model checking

By Anissa Kheireddine, Étienne Renault, Souheib Baarir

2022-12-09

In Proceedings of the 29th asia-pacific software engineering conference (APSEC’22)

Abstract Bounded model checking (BMC) aims at checking whether a model satisfies a property. Most of the existing SAT-based BMC approaches rely on generic strategies, which are supposed to work for any SAT problem. The key idea defended in this paper is to tune SAT solvers algorithm using: (1) a static classification based on the variables used to encode the BMC into a Boolean formula; (2) and use the hierarchy of Manna&Pnueli that classifies any property expressed through Linear-time Temporal Logic (LTL).

From Spot 2.0 to Spot 2.10: What’s new?

By Alexandre Duret-Lutz, Étienne Renault, Maximilien Colange, Florian Renkin, Alexandre Gbaguidi Aisse, Philipp Schlehuber-Caissier, Thomas Medioni, Antoine Martin, Jérôme Dubois, Clément Gillard, Henrich Lauko

2022-06-06

In Proceedings of the 34th international conference on computer aided verification (CAV’22)

Abstract Spot is a C++17 library for LTL and $\omega$-automata manipulation, with command-line utilities, and Python bindings. This paper summarizes its evolution over the past six years, since the release of Spot 2.0, which was the first version to support $\omega$-automata with arbitrary acceptance conditions, and the last version presented at a conference. Since then, Spot has been extended with several features such as acceptance transformations, alternating automata, games, LTL synthesis, and more.

LTL under reductions with weaker conditions than stutter invariance

By Emmanuel Paviot-Adet, Denis Poitrenaud, Étienne Renault, Yann Thierry-Mieg

2022-04-18

In Proceedings of the 41th IFIP international conference on formal techniques for distributed objects, components and systems (FORTE’22)

Abstract Verification of properties expressed as omega-regular languages such as LTL can benefit hugely from stutter insensitivity, using a diverse set of reduction strategies. However properties that are not stutter invariant, for instance due to the use of the neXt operator of LTL or to some form of counting in the logic, are not covered by these techniques in general. We propose in this paper to study a weaker property than stutter insensitivity.

Towards better heuristics for solving bounded model checking problems

By Anissa Kheireddine, Étienne Renault, Souheib Baarir

2021-08-31

In Proceedings of the 27th international conference on principles and practice of constraint programmings (CP’21)

Abstract This paper presents a new way to improve the performance of the SAT-based bounded model checking problem by exploiting relevant information identified through the characteristics of the original problem. This led us to design a new way of building interesting heuristics based on the structure of the underlying problem. The proposed methodology is generic and can be applied for any SAT problem. This paper compares the state-of-the-art approach with two new heuristics: Structure-based and Linear Programming heuristics and show promising results.

Go2Pins: A framework for the LTL verification of Go programs

By Alexandre Kirszenberg, Antoine Martin, Hugo Moreau, Étienne Renault

2021-06-08

In Proceedings of the 27th international SPIN symposium on model checking of software (SPIN’21)

Abstract We introduce Go2Pins, a tool that takes a program written in Go and links it with two model-checkers: LTSMin [19] and Spot [7]. Go2Pins is an effort to promote the integration of both formal verifica- tion and testing inside industrial-size projects. With this goal in mind, we introduce black-box transitions, an efficient and scalable technique for handling the Go runtime. This approach, inspired by hardware ver- ification techniques, allows easy, automatic and efficient abstractions.

Improving swarming using genetic algorithms

By Étienne Renault

2020-06-02

In Innovations in Systems and Software Engineering: a NASA journal (ISSE)

Abstract The verification of temporal properties against a given system may require the exploration of its full state space. In explicit model checking, this exploration uses a depth-first search and can be achieved with multiple randomized threads to increase performance. Nonetheless, the topology of the state space and the exploration order can cap the speedup up to a certain number of threads. This paper proposes a new technique that aims to tackle this limitation by generating artificial initial states, using genetic algorithms.

Combining parallel emptiness checks with partial order reductions

By Denis Poitrenaud, Étienne Renault

2019-08-02

In Proceedings of the 21st international conference on formal engineering methods (ICFEM’19)

Abstract In explicit state model checking ofconcurrent systems, multicore emptiness checks and partial order reductions (POR) are two major techniques to handle large state spaces. The first one tries to take advantage of multi-core architectures while the second one may decrease exponentially the size of the state space to explore. For checking LTL properties, Bloemen and van de Pol [2] shown that the best performance is currently obtained using their multi-core SCC-based emptiness check.

Improving parallel state-space exploration using genetic algorithms

By Étienne Renault

2018-06-14

In Proceedings of the 12th international conference on verification and evaluation of computer and communication systems (VECOS’18)

Abstract The verification of temporal properties against a given system may require the exploration of its full state space. In explicit model-checking this exploration uses a Depth-First-Search (DFS) and can be achieved with multiple randomized threads to increase performance. Nonetheless the topology of the state-space and the exploration order can cap the speedup up to a certain number of threads. This paper proposes a new technique that aims to tackle this limitation by generating artificial initial states, using genetic algorithms.

Go2Pins: A framework for the LTL verification of Go programs (extended version)

Towards better heuristics for solving bounded model checking problems

Tuning SAT solvers for LTL model checking

From Spot 2.0 to Spot 2.10: What’s new?

LTL under reductions with weaker conditions than stutter invariance

Towards better heuristics for solving bounded model checking problems

Go2Pins: A framework for the LTL verification of Go programs

Improving swarming using genetic algorithms

Combining parallel emptiness checks with partial order reductions

Improving parallel state-space exploration using genetic algorithms

Search

Tags