Effective Techniques for Stateless Model Checking

Autor: Aronis, Stavros

Stateless model checking is a technique for testing and verifying concurrent programs, based on exploring the different ways in which operations executed by the processes of a concurrent program can be scheduled. The goal of the technique is to expos

Externí odkaz: http://urn.kb.se/resolve?urn=urn:nbn:se:uu:diva-333541

Stateless Model Checking for TSO and PSO

Autor: Abdulla, Parosh, Aronis, Stavros, Atig, Mohammed Faouzi, Jonsson, Bengt, Leonardsson, Carl, Sagonas, Konstantinos

We present a technique for efficient stateless model checking of programs that execute under the relaxed memory models TSO and PSO. The basis for our technique is a novel representation of executions under TSO and PSO, called chronological traces. Ch

Externí odkaz: http://arxiv.org/abs/1501.02069

Stateless model checking for TSO and PSO.

Autor: Abdulla, Parosh¹ parosh@it.uu.se, Aronis, Stavros¹ stavros.aronis@it.uu.se, Atig, Mohamed¹ mohamed_faouzi.atig@it.uu.se, Jonsson, Bengt¹ bengt.jonsson@it.uu.se, Leonardsson, Carl¹ carl.leonardsson@it.uu.se, Sagonas, Konstantinos¹ konstantinos.sagonas@it.uu.se

Publikováno v: Acta Informatica. Dec2017, Vol. 54 Issue 8, p789-818. 30p.

Stateless Model Checking for TSO and PSO.

Autor: Abdulla, Parosh Aziz, Aronis, Stavros, Atig, Mohamed Faouzi, Jonsson, Bengt, Leonardsson, Carl, Sagonas, Konstantinos

Publikováno v: Tools & Algorithms for the Construction & Analysis of Systems 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory & Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings; 2015, p353-367, 15p

On Using Erlang for Parallelization.

Autor: Aronis, Stavros, Sagonas, Konstantinos

Publikováno v: Trends in Functional Programming (9783642404467); 2013, p295-310, 16p