Description#

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#

• Formal Methods Seminar at Loria
• Security Seminar at Loria
• ACNS 2014, 12th International Conference on Applied Cryptography and Network Security
• POST 2014, 3rd Conference on Principles of Security and Trust
• Sec@SAC 2014, Computer Security track at the 29th ACM Symposium on Applied Computing

Past Events#

• FroCoS 2013, 9th International Symposium on Frontiers of Combining Systems
• CADE 2013, 24th International Conference on Automated Deduction
• LATA 2013, 7th International Conference on Language and Automata Theory and Applications
• GRSRD 2013 -Grande Region Security and Reliability Day
• AFADL-CIEL-GPL 2013

• GRSRD 2012, Grande Region Security and Reliability Day
• POST 2012, First Conference on Principles of Security and Trust, one of the ETAPS 2012 conferences
• ISPEC 2012, 8th Information Security Practice and Experience Conference
• ACNS 2012, 10th International Conference on Applied Cryptography and Network Security
• CSF 2012, 25th Computer Security Foundations Symposium
• IJCAR 2012 The 6th International Joint Conference on Automated Reasoning
• TGC 2012 The 7th Symposium on Trustworthy Global Computing
• FSTTCS 2012 The 32nd Conference on Foundations of Software Technology and Theoretical Computer Science

• 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.

News#

• The research activity reports of our group are available: 2007, 2008, 2009, 2010, 2011, 2012, 2013,

2014