Homepage of Carl Leonardsson

carl_256.jpg

I am currently studying for a PhD in Algorithmic Verification at Uppsala University. My supervisor is Bengt Jonsson.

Room: 1421 Polacksbacken
Mail: mail.png

Table of Contents

Research

I am working on automated verification of safety properties in parallel algorithms running under weak memory models, as well as automated inference of memory barriers that are necessary to ensure the correctness of such algorithms.

Project Home

Publications

  1. Counter-Example Guided Fence Insertion under TSO, Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Carl Leonardsson and Ahmed Rezine, TACAS 2012
  2. Automatic fence insertion in integer programs via predicate abstraction, Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Carl Leonardsson, and Ahmed Rezine. In SAS, volume 7460 of LNCS. Springer, 2012.
  3. (Tool demo) Memorax, a Precise and Sound Tool for Automatic Fence Insertion under TSO, Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Carl Leonardsson, and Ahmed Rezine. In TACAS, volume 7795 of LNCS. Springer, 2013.
  4. Stateless Model Checking for TSO and PSO, Parosh Aziz Abdulla, Stavros Aronis, Mohamed Faouzi Atig, Bengt Jonsson, Carl Leonardsson, and Konstantinos Sagonas. In TACAS, volume 9035 of LNCS. Springer, 2015. (A technical report is available on arXiv.)

Tools

Nidhugg

(GitHub)

A bug-finding tool for analysis of programs written in C/pthreads, running under the SC, TSO or PSO memory models. Nidhugg implements the stateless model checking technique described in publication 4 above.

Installation instructions as well as a manual can be found on the GitHub page.

Memorax

(GitHub, Manual)

A prototype tool for analysis of programs under the TSO memory model. Memorax implements the techniques of publications 1 and 2 above. It allows automatic reachability analysis, as well as automatic inference of memory barriers that are necessary in a program to satisfy given safety properties.

Memorax should compile in UNIX-like environments providing the following requirements:

  • A C++ compiler supporting C++11. For example g++ version 4.6 or higher.
  • In order to run the graphical interface, python is required at a version of 2.6 or higher installed with tcl/tk of version 8.4 or higher. (On debian based systems, install the package python-tk.)
  • For predicate abstraction the MathSAT SMT solver as well as the library gmpxx are required. Memorax supports MathSAT 4 and MathSAT 5. MathSAT 4 is recommended. Memorax can be compiled without MathSAT and gmpxx, but will then not support predicate abstraction.
  • To be able to graphically draw automata, Graphviz is required.

Compilation follows the usual pattern: ./configure ; make ; make install. The README file contains details.

If you encounter problems or bugs when installing or running Memorax, your feedback by email will be appreciated.

Memorax is released as open source under the GNU General Public License version 3.