Computer Aided Verification

Computer Aided Verification (CAV)
Type Conférence académique
Création 1989
Localisation alternativement en Amérique du Nord et en Europe
Date annuelle, en juillet
Site web http://cavconference.org
modifier 

La conférence Computer Aided Verification (abrégé en CAV) est un congrès scientifique annuel sur la théorie et la pratique de l'analyse formelle assistée par ordinateur de logiciels et matériels. C'est une des conférences les mieux classées en informatique[1],[2].

Plusieurs articles historiques sur les techniques de vérification de modèles ont été présentés à CAV, tels que « Counterexample-Guided Abstraction Refinement »[3] et des méthodes de réduction par ordre partiel comme « A Stubborn Attack On State Explosion »[4],[5].

Description

CAV est la conférence internationale principale sur la vérification assistée par ordinateur. Elle offre un forum de présentation de recherches avancées allant de la vérification de modèles et de la démonstration automatique de théorèmes aux tests. Les recherches présentées à CAV comprennent l'application de méthodes formelles à de nombreuses variétés de systèmes, y compris le matériel, les logiciels et les protocoles de communication. Elle couvre de nombreux modèles de systèmes, y compris les systèmes à états finis et à états infinis, les systèmes hybrides et les systèmes probabilistes. Elle comprend à la fois des études de cas théoriques et des études de cas industriels. Le point commun est l'utilisation de méthodes automatiques pour aider les concepteurs à construire des systèmes plus fiables.

Organisation

CAV a lieu chaque année en juillet, et alternativement en l'Amérique du Nord et l'Europe. Elle a débuté sous la forme d'un workshop qui s'est tenu en 1989 à Grenoble. Par la suite, CAV a été organisée comme une conférence par Edmund Clarke, Robert Kurshan, Amir Pnueli ou Joseph Sifakis. En général, chaque conférence comporte un ou plusieurs exposés par des conférenciers invités. Un jour de la conférence, le tutorial day, est consacré à des exposés de synthèse ou tutoriels. Tout un ensemble de workshop forment un essaim de conférences satellites autour de la conférence principale. En 2018, on en dénombre douze[6] :

  • workshop on Formal Reasoning in Distributed Algorithms (FRIDA)
  • workshop on Runtime Verification for Rigorous Systems Engineering (RV4RISE)
  • le 5e workshop on Horn Clauses for Verificationand Synthesis (HCVS)
  • le 7e workshop on Synthesis (SYNT)
  • l'International Workshop on Parallel Logical Reasoning (PLR),
  • la 10e working Conference on Verified Software: Theories, Tools and Experiments (VSTTE)
  • le workshop on Machine Learning for Programming (MLP)
  • le 11e International Workshop on Numerical Software Verification (NSV),
  • le workshop on Verification of Engineered Molecular Devices and Programs (VEMDP),
  • le 3e workshop on Fun With FormalMethods (FWFM),
  • le workshop on Robots, Morality, and Trust through the Verification Lens,
  • et l'IFAC Conference on Analysis and Design of Hybrid Systems(ADHS)

Les actes de la conférence sont publiées par Springer-Verlag dans la série des Lecture Notes in Computer Science, en 2018 pour la première fois en accès ouvert. Une sélection d'articles tirés des communications est publiée dans un numéro spécial de Formal Methods in System Design et dans le Journal of the ACM.

Prix CAV

Chaque année, un prix CAV[7] est attribué lors de la conférence. Le montant du prix est de 10 000 à partager entre les récipiendaires s'il y en a plusieurs. Les premiers lauréats, en 2008, étaient Rajeev Alur et David L. Dill, en 2018 ils étaient six à se partager le prix : Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Daniel Kroening, Flavio Lerda et Yunshan Zhu[7].

Sélection

À titre d'exemple, la conférence 2018 a reçu 215 propositions ; le comité de sélection a retenu 13 articles sur des outils et 52 communications normales, ce qui donne un taux d'acceptation de l'ordre de 30%, montrant que la sélection a été très forte.

Références

  1. ↑ « Ranked Conference List (2010) », Australian Research Council (consulté le )
  2. ↑ « Top conferences in Software Engineering », Microsoft Academic Search (en) (consulté le )
  3. ↑ Edmund M. Clarke, « Counterexample-Guided Abstraction Refinement », Lecture Notes in Computer Science, vol. 1855 « Proceedings CAV 2000 »,‎ , p. 154–169 (ISBN 978-3-540-67770-3, DOI 10.1007/10722167_15).
  4. ↑ Antti Valmari, « A Stubborn Attack On State Explosion », Lecture Notes in Computer Science, vol. 531 « Proceedings CAV 1990 »,‎ , p. 156–165 (ISBN 978-3-540-54477-7, DOI 10.1007/BFb0023729)
  5. ↑ Patrice Godefroid, « Using Partial Orders to Improve Automatic Verification Methods », Lecture Notes in Computer Science, vol. 531 « Proceedings CAV 1990 »,‎ , p. 176–185 (ISBN 978-3-540-54477-7, DOI 10.1007/BFb0023731).
  6. ↑ Préface des actes de CAV 2018
  7. ↑ a et b « CAV Award »

Article lié

Liens externes