CASSIS : Combining ApproacheS for the Security of Infinite state Systems#

The CASSIS project ended in Dec. 2015. The follow-up project is PESTO.


The aim of the project is the design and the development of tools for checking the safety of systems with an infinite number of states. Our analysis of systems is based on a symbolic representation of the sets of states as formal languages or logical formulas. Safety is obtained by automated proofs, symbolic exploration of models, or tests generation. An originality of the project lies in its focus on the infinite systems, parameterized or of large size, where each technique taken separately shows its limits. As examples of such systems we can mention protocols operating on topologies of arbitrary size (ring networks), systems handling datastructures with unspecified size (sets), or whose control is infinite (automata communicating by unlimited buffers).

The applications are embedded softwares on smart cards, for example, security protocols and distributed systems.

Research Domains#

Our goal is designing methods and building tools for checking critical software. To this end, we combine techniques from
  • Automated deduction
  • Synthesis and constraint solving
  • Analysis of reachability in infinite systems

Application Domains#

The current application domains of the team are:
  • Verification of security protocols
  • Generation of tests sequences from a formal model
  • Verification and debugging of programs

Upcoming Events#

Past Events#

  • 23rd International Conference on Automated Deduction, CADE 2011
  • 6th International Conference on Risks and Security of Internet and Systems, CriSIS 2011
  • 8th International Symposium on Frontiers of Combining Systems, FroCoS 2011
  • Workshop on Theory of Security and Applications, (TOSCA 2011), Saarbruecken, Germany, March 31 - April 1, 2011.
  • 2011 Grande Region Security and Reliability Day, Trier, Germany, March 25, 2011.
  • 6th ACM Symposium on Information, Computer and Communications Security (ASIACCS 2011), Hong Kong, March 22-24, 2011.
  • Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010), Chennai, India, December 15-18, 2010.
  • 17th ACM Conference on Computer and Communications Security, Chicago, USA, October 4-8, 2010.
  • 8th International Workshop on Security Issues in Concurrency (SecCo 2010), Paris, France, August 30, 2010 (co-located with CONCUR 2010).
  • 5th International Joint Conference on Automated Reasoning (IJCAR 2010), Edinburgh, Scotland, UK, July 16-19, 2010.
  • Workshop on Foundations of Security and Privacy (FCS-PrivMod 2010), Edinburgh, Scotland, UK, July 14-15, 2010.
  • 25th Annual IEEE Symposium on Logic in Computer Science (LICS 2010), Edinburgh, Scotland, UK, July 11-14, 2010.
  • Modelling and Verifying Parallel Processes (MoVeP 2010 summer school), Aachen, Germany, June 28 - July 2, 2010.
  • 7th International Symposium on Frontiers of Combining Systems (FroCoS 2009), Trento, Italy, September 16-18, 2009.
  • 22nd International Conference on Automated Deduction (CADE-22), Montreal, Canada, August 2-7, 2009.
  • 22nd IEEE Computer Security Foundations Symposium (CSF 2009), Port Jefferson, USA, July 8-10, 2009.
  • International Workshop on First-Order Theorem Proving (FTP 2009), Oslo, Norway, July 6-7, 2009.
  • 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2009), York, UK, March 22-29, 2009.
  • Joint Workshop on Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security (ARSPA-WITS'09), York, UK, March 2009. Affiliated with ETAPS 2009.
  • Luxembourg Day on Security and Reliability, University Campus Kirchberg, Luxembourg city, Luxembourg, February 10, 2009.
  • Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'09), Savannah, GA, USA (co-located with POPL 2009), January 18-20, 2009.



Add new attachment

Only authorized users are allowed to upload new attachments.
« This page (revision-103) was last changed on 12-mai-2016 20:52 by Steve Kremer