graph based verification
This research line consists regards model checking approaches where:
- systems are described by means of graph, graph transformation systems (aka graph rewrite systems, aka graph grammars)
- system properties are specified by means of logics that involve structural (or spatial) and temporal modal operators
- verification algorithms deal with graphical nature of models and their specificaiton
More details on this topic can be found in the following documents and the references therein:
- Counterpart semantics for a second-order mu-calculus
Fabio Gadducci, Alberto Lluch Lafuente, Andrea Vandin
International Conference on Graph Transformation (ICGT’10)
draft - Graphical Encoding of a Spatial Logic for the pi-calculus
Fabio Gadducci, Alberto Lluch Lafuente, Proceeedings of the 2nd Conference on Algebra and Coalgebra in Computer Science (CALCO’07), 2007.
abstract pdf bib - A Temporal Graph Logic for the Verification of Graph Transformation Systems
Paolo Baldan, Andrea Corradini, Barbara König, Alberto Lluch Lafuente, WADT’06, 2007.
abstract pdf bib slides - Heuristic Search for the Analysis of Graph Transition Systems
Stefan Edelkamp, Shahid Jabbar, Alberto Lluch Lafuente, International Conference on Graph Transformation (ICGT) Natal, 2006.
abstract pdf bib slides - A Logic for Application Level QoS
Dan Hirsch, Alberto Lluch-Lafuente, Emilio Tuosto, Proceedings of the 3rd Workshop on Quantitative Aspects of Programming Languages, Elsevier Electronic Notes on Theoretical Computer Science, 2006.
abstract pdf bib - Graphical Verification of a Spatial Logic for the pi-calculus
Fabio Gadducci, Alberto Lluch, 1st Workshop on Graph Transformation for Verification and Concurrency (GT-VC 2005), August 2005.
abstract pdf bib - A logic for graphs with QoS
Gianluigi Ferrari, Alberto Lluch Lafuente, 1st Workshop on Views On Designing Complex Architectures, September 2004.
abstract pdf bib slides
