Archive pour la catégorie 'Manifestations'

Session AFSEC pendant les journées du GDR GPL

Monday 7 June 2021

Les journées du GDR GPL se tiendront du lundi 14 au vendredi 18 juin prochain, à distance. À cette occasion, une session AFSEC sera organisée le mercredi 16 juin de 13h30 à 15h30. Deux exposés sur la thématique des solveurs SMT seront donnés. Pour s’inscrire c’est ici :

On the Combination of Polyhedral Abstraction and SMT-based Model Checking for Petri nets (par Nicolas Amat)

We define a method for taking advantage of net reductions in combination with a SMT-based model checker. We prove the correctness of this method using a new notion of equivalence between nets that we call polyhedral abstraction. Our approach has been implemented in a tool, named SMPT, that provides two main procedures: Bounded Model Checking (BMC) and Property Directed Reachability (PDR). Each procedure has been adapted in order to use reductions and to work with arbitrary Petri nets. We tested SMPT on a large collection of queries used during the 2020 edition of the Model Checking Contest. Our experimental results show that our approach works well, even when we only have a moderate amount of reductions.

SMT-Based Bounded Model Checking of Max-Plus Linear Systems (par Muhammad Syifa’ul Mufid)

Max-Plus Linear (MPL) systems are an algebraic formalism with practical applications in transportation networks, manufacturing and biological systems. MPL systems can be naturally modeled as infinite-state transition systems, and exhibit interesting structural properties (e.g. periodicity or steady-state), for which analysis methods have been recently proposed. In this talk, we tackle the open problem of specifying and analyzing user-defined temporal properties for MPL systems. We propose Time-Difference LTL (TDLTL), a logic that encompasses the delays between the discrete-time events governed by an MPL system, and characterizes the problem of model checking TDLTL over MPL. We propose a family of specialized algorithms leveraging the periodic behaviour of an MPL system. We prove soundness and completeness, showing that the transient and cyclicity of the MPL system induce a completeness threshold for the verification problem. The algorithms are cast in the setting of SMT-based verification of infinite-state transition systems over the reals, with variants depending on the computation of the bound, and on the unrolling of the transition relation. Our comprehensive experiments show that the proposed techniques can be applied to MPL systems of large dimensions and on general TDLTL formulae, with remarkable performance gains against a dedicated abstraction-based technique and a translation to the nuXmv symbolic model checker.

Publié dans Actions Afsec, Journées, Manifestations | Pas de commentaire »

ISoLA 2010 et WCTT Track

Friday 10 September 2010

La conférence ISoLA 2010 (4th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation 18-20 October 2010) a un track WCTT (Worst Case Traversal Time). La communauté AFSEC/WEED y est particulièrement bien représentée avec 5 papiers sur 9.

Publié dans Actions Afsec, Conférences, Conférences, Manifestations, WEED | Pas de commentaire »

FSTTCS 2010 (15-18 septembre 2010)

Sunday 13 June 2010

Foundations of Software Technology and Theoretical Computer Science

December 15 to 18, 2010,
IMSc, Chennai, India

Soumission des articles : 07 juillet 2010
Notification de l’acceptation : 13 septembre 2010

Publié dans Conférences, Manifestations | Pas de commentaire »

MOVEP 2010 (June 28 — July 2 2010)

Monday 17 May 2010

MOVEP 2010
9th International Summer School on
MOdelling and VErifying parallel Processes

June 28 — July 2 2010, Aachen, Germany

The purpose of MOVEP is to bring together researchers, students and people from industry working in the fields of control and verification of concurrent and reactive systems. The school seeks to offer a broad spectrum of current research in this area of theoretical and applied computer science. The topics covered by MOVEP 2010 include model checking, testing, synthesis, real-time and hybrid systems, games, stochastic systems, security, computational systems biology etc.

MOVEP 2010 is supported by the ESF GAMES project, INRIA Rennes, Action AFSEC (CNRS) and the RWTH Aachen.

Publié dans Actions Afsec, Ecoles d'été, Manifestations | Pas de commentaire »

RTSS 2010 (30 nov – 03 dec 2010)

Thursday 13 May 2010

The 31st IEEE Real-Time Systems Symposium

RTSS 2010
November 30 – December 3, 2010
San Diego, CA, USA

Soumission des articles : 16 mai 2010
Notification de l’acceptation : 08 aout 2010

Publié dans Conférences, Manifestations | Pas de commentaire »

FORMATS 2010 (8-10 Septembre 2010)

Thursday 13 May 2010

The 8th International Conference on Formal Modelling and Analysis of Timed Systems.

IST Austria, Klosterneuburg, Austria
8-10 September, 2010

Soumission des articles : 25 avril 2010
Notification de l’acceptation : 24 mai 2010

Publié dans Conférences, Manifestations | Pas de commentaire »

Petri NETS 2010 (23 au 25 juin 2010)

Sunday 25 October 2009

31st International Conference on Application and Theory of Petri Nets and other Models of Concurrency


June 21-25, 2010
Braga, Portugal

. Submission of Papers : January 5, 2010
. Notification : March 1, 2010
. Final Version Due : April 1, 2010
. Workshops & Tutorials : June 21-22, 2010
. Conference : June 23-25, 2010

Publié dans Conférences, Manifestations | Pas de commentaire »

ETAPS 2010 (du 20 au 28 Mars 2010)

Monday 24 August 2009

The European Joint Conferences on Theory and Practice of Software (ETAPS) is a confederation of five main annual conferences :
CC 2010, International Conference on Compiler Construction
ESOP 2010, European Symposium on Programming
FASE 2010, Fundamental Approaches to Software Engineering
FOSSACS 2010, Foundations of Software Science and Computation Structures
TACAS 2010, Tools and Algorithms for the Construction and Analysis of Systems

20-28 March 2010, Paphos, Cyprus

ETAPS 2010

Soumission des articles : 8 octobre 2009
Notification de l’acceptation : 11 decembre 2009

Publié dans Conférences, Manifestations | Pas de commentaire »

FSTTCS 2009 (15-17 décembre 2009)

Thursday 4 June 2009

The 29th Foundations of Software Technology and Theoretical Computer Science Conference

December 15 to 17, 2009, IIT Kanpur, India


Soumission des articles : 7 juillet 2009
Notification de l’acceptation : 14 septembre 2009

Publié dans Conférences, Manifestations | Pas de commentaire »

RTSS’09 (1-4 decembre 2009)

Monday 4 May 2009

The 30th IEEE Real-Time Systems Symposium

Washington, D.C., USA, December 1-4, 2009

RTSS 2009

Soumission des articles : 26 mai 2009
Notification de l’acceptation : 23 aout 2009

Publié dans Conférences, Manifestations | Pas de commentaire »