Program verification

Researchers

• Mads Dam
• Dilian Gurov

Ph.D. Students

• Pedro de Carvalho Gomes
• Siavash Soleimanifard

Alumni

• Andreas Lundblad Ph. D. 2013
• Irem Aktug Ph. D. 2008
• Gena Chugunov Ph. Lic. 2004
• Lars-aake Fredlund Ph. D. 2001

Short description

Control flow analysis

A collaborative project aiming at the development of techniques for the algorithmic verification of control flow based properties of programs with procedures, with the focus on compositionality. The project is carried out in the context of the Verification of Control-Flow Properties of Programs with Procedures (CVPP) project.

Provably correct extraction of software models

The project researches methods to generate synthetic software models, which are suitable for formal verification techniques. It is a joint project with research partners in University of Twente.

Currently the project extracts control-flow graphs, a common software model which preserves control-flow information. The extraction is formally proven to be correct with respect to safety control-flow properties. The outcome has been the CFGEx tool, which extracts control-flow graphs from Java bytecode. The on-going research is extending CFGEx to a modular set-up, and also to extract models from another software languages.

Projects and Funding

TBD

Publications

• Algorithmic Verification of Procedural Programs in the Presence of Code Variability
  Siavash Soleimanifard and Dilian Gurov
  Technical report. 2013.
  
• Reducing behavioural to structural properties of programs with procedures
  Dilian Gurov and Marieke Huisman
  In Theoretical Computer Science. 2013.
  
• Procedure-Modular Specification and Verification of Temporal Safety Properties
  Siavash Soleimanifard, Dilian Gurov and Marieke Huisman
  In Software and Systems Modeling. 2013.
  
• Sound Modular Extraction of Control Flow Graphs from Java Bytecode
  Pedro de Carvalho Gomes
  Licentiate Thesis. 2012.
  
• Sound Control-Flow Graph Extraction for Java Programs with Exceptions
  Afshin Amighi, Pedro de Carvalho Gomes, Dilian Gurov, and Marieke Huisman
  In Proceedings of SEFM. 2012.
  
• Procedure-Modular Verification of Temporal Safety Properties
  Siavash Soleimanifard
  Licentiate Thesis. 2012.
  
• Provably Correct Control-Flow Graphs from Java programs with Exceptions
  A. Amighi, P. de Carvalho Gomes, Dilian Gurov and M. Huisman.
  Technical Report. 2012.
  
• ProMoVer: Modular Verification of Temporal Safety Properties
  Siavash Soleimanifard, Dilian Gurov, and Marieke Huisman
  In 9th International Conference on Software Engineering and Formal Methods (SEFM) 2011.
  Lecture Notes in Computer Science, vol. 7041, pp. 366-381, 2011
• Compositional Algorithmic Verification of Software Product Lines
  Ina Schaefer, Dilian Gurov, and Siavash Soleimanifard
  In Post-proceedings of: FMCO'10
  Lecture Notes in Computer Science, vol. 6957, pp. 184-203, 2011
• CVPP: A Tool Set for Compositonal Verification of Control-Flow Safety Properties
  Marieke Huisman, and Dilian Gurov
  In Proceedings of: FoVeOOS'10, 2010
• Procedure-Modular Verification of Control Flow Safety Properties
  Siavash Soleimanifard, Dilian Gurov, and Marieke Huisman
  In Proceedings of: FTfJP'10, 2010
• Reducing Behavioural to Structural Properties of Programs with Procedures
  Dilian Gurov  and  Marieke Huisman
  In Proceedings of: VMCAI'09
  Lecture Notes in Computer Science, vol. 5403, pp. 136-150, 2009 (tool web-interface) (slides)
  Full version available as: Technical Report TRITA-CSC-TCS 2007:3, December 2007
  
• Program Models for Compositional Verification
  Marieke Huisman, Irem Aktug, and Dilian Gurov
  In Proceedings of: ICFEM'08
  Lecture Notes in Computer Science, vol. 5256, pp. 147-166, 2008
• Compositional Verification of Sequential Programs with Procedures
  Dilian Gurov, Marieke Huisman, and Christoph Sprenger
  Journal of Information and Computation, vol. 206, no. 7, pp. 840-868, 2008
• Composing Modal Properties of Programs with Procedures
  Marieke Huisman, and Dilian Gurov
  In Proceedings of: FESCA'07
  Electronic Notes in Theoretical Computer Science, vol. 203, issue 7, pp. 87-101, 2009 (slides)
  
• Interface Abstraction for Compositional Verification
  Dilian Gurov, and Marieke Huisman
  In Proceedings of: SEFM'05
  IEEE Computer Society, pp. 414-423, 2005 (slides)
• Compositional Verification for Secure Loading of Smart Card Applets
  Christoph Sprenger, Dilian Gurov, and Marieke Huisman
  In Proceedings of: Memocode'04
  IEEE Formal Methods and Models for Co-Design, pp. 211-222, 2004
• Checking Absence of Illicit Applet Interactions: A Case Study
  Marieke Huisman, Dilian Gurov, Christoph Sprenger, and Gennady Chugunov
  In Proceedings of: FASE'04  [337]
  Lecture Notes in Computer Science, vol. 2984, pp. 84-98
  Winner of the EASST award for Best Software Science Paper, 2004 (slides)
• Simulation Logic, Applets and Compositional Verification
  Christoph Sprenger, Dilian Gurov, and Marieke Huisman
  INRIA Technical Report RR-4890, 2003
• Model Checking of Multi-Applet JavaCard Applications
  Gennady Chugunov, Lars-Åke Fredlund, and Dilian Gurov
  In Proceedings of: CARDIS'02 [534]
  USENIX Publications, pp. 87-95, 2002 (slides)
• Compositional Verification of Secure Applet Interactions
  Gilles Barthe, Dilian Gurov, and Marieke Huisman
  In Proceedings of: FASE'02 [337]
  Lecture Notes in Computer Science, vol. 2306, pp. 15-32, 2002 (slides)
• Compositional Specification and Verification of Control Flow
  Based Security Properties of Multi-Application Programs
  Gilles Barthe, Dilian Gurov, and Marieke Huisman
  In Proceedings of: FTfJP'01, 2001