Annual Conference: Communicating Process Architectures
Communicating Process Architectures 2018,
the 40th. WoTUG conference on concurrent and parallel systems, takes place from
Sunday August 19th. to Wednesday August 22nd. 2018 and is hosted by
Professor Dr. Rainer Spallek,
VLSI Design, Diagnostics and Architecture
at the Faculty of Computer Science,
Technische Universität Dresden, Germany.
The conference is organised by Dr. Spallek in collboration with Oliver Knodel and Uwe Mielke
and in partnership with WoTUG.
WoTUG provides a forum for the discussion and promotion of concurrency ideas,
tools and products in computer science.
It organises specialist workshops and annual conferences that address
key concurrency issues at all levels of software and hardware granularity.
WoTUG aims to progress the leading state of the art in:
and to stimulate discussion and ideas on the roles concurrency will play in the future:
theory (programming models, process algebra, semantics, ...);
practice (multicore processors and run-times, clusters, clouds, libraries, languages, verification, model checking, ...);
education (at school, undergraduate and postgraduate levels, ...);
applications (complex systems, modelling, supercomputing, embedded systems, robotics, games, e-commerce, ...);
Of course, neither of the above sets of bullets are exclusive.
for the next generation of scalable computer infrastructure (hard and soft) and application,
where scaling means the ability to ramp up functionality (stay in control as complexity increases)
as well as physical metrics (such as absolute performance and response times);
for system integrity (dependability, security, safety, liveness, ...);
for making things simple.
A database of papers and presentations from WoTUG conferences is here.
The Abstract below has been randomly selected from this database.
Combining Partial Order Reduction with Bounded Model Checking
Model checking is an efficient technique for verifying properties on
reactive systems. Partial-order reduction (POR) and symbolic model
checking are two common approaches to deal with the state space
explosion problem in model checking. Traditionally, symbolic model
checking uses BDDs which can suffer from space blow-up. More recently
bounded model checking (BMC) using SAT-based procedures has been used
as a very successful alternative to BDDs. However, this approach
gives poor results when it is applied to models with a lot of
asynchronism. This paper presents an algorithm which combines
partial order reduction methods and bounded model checking techniques
in an original way that allows efficient verification of temporal
logic properties (LTL_X) on models featuring asynchronous processes.
The encoding to a SAT problem strongly reduces the complexity and
non-determinism of each transition step, allowing efficient analysis
even with longer execution traces. The starting-point of our work is
the Two-Phase algorithm (Namalesu and Gopalakrishnan) which performs
partial-order reduction on process-based models. At first, we adapt
this algorithm to the bounded model checking method. Then, we describe
our approach formally and demonstrate its validity. Finally, we
present a prototypal implementation and report encouraging
experimental results on a small example.