Verimag

by kinds

Journal Articles

2014

  1. Apport des méthodes formelles pour l'exploitation des logs informatiques dans un contexte contractuel. Gregor Goessler, Daniel Le Métayer, Eduardo Mazza, Marie-Laure Potet, Lacramioara Astefanoaei - TSI, Technique et Science Informatiques - [bibtex]
  2. Implementing and Reasoning About Hash-consed Data Structures in Coq. Thomas Braibant, Jacques-Henri Jourdan, David Monniaux - Journal of Automated Reasoning - [bibtex]
  3. Deciding Conditional Termination. Marius Bozga, Radu Iosif, Filip Konecn\'y - Logical Methods in Computer Science - [bibtex]
  4. Analyse de Code et Recherche de Vulnérabilités. Marie-Laure Potet, Josselin Feist, Laurent Mounier - Revue MISC - [bibtex]
  5. Statically detecting Use-After-Free on Binary Code. Josselin Feist, Laurent Mounier, Marie-Laure Potet - Journal of Computer Virology and Hacking Techniques - [bibtex]

2013

  1. Automata-Based Termination Proofs. Radu Iosif, Adam Rogalewicz - Computing and Informatics - [bibtex]

2012

  1. Generating Invariant-based Certificates for Embedded Systems. Jan-Olaf Blech, Michaël Périn - ACM Transactions on Embedded Computing Systems (TECS) - [bibtex]
  2. Politiques de gestion de protections pour l'implémentation de sections critiques.. Sifakis Emmanuel, Mounier Laurent - Techniques et Sciences Informatiques - [bibtex]
  3. More testable properties. Ylies Falcone, Jean-Claude Fernandez, Thierry Jéron, Hervé Marchand, Laurent Mounier - STTT - [bibtex]
  4. Introduction à la calculabilité. David Monniaux - Quadrature - [bibtex]
  5. Invariant Generation through Strategy Iteration in Succinctly Represented Control Flow Graphs. Thomas Gawlitza, David Monniaux - Logical Methods in Computer Science - [bibtex]
  6. Synchronous Programming of Device Drivers for Global Resource Control in Embedded Operating Systems. Nicolas Berthier, Florence Maraninchi, Laurent Mounier - ACM Transactions on Embedded Computing Systems (TECS) - [bibtex]

2011

  1. Programs with lists are counter automata. Ahmed Bouajjani, Marius Bozga, Peter Habermehl, Radu Iosif, Pierre Moro, Tomás Vojnar - Formal Methods in System Design - [bibtex]
  2. Liability issues in software engineering: the use of formal methods to reduce legal uncertainties. Daniel Le Métayer, Manuel Maarek, Eduardo Mazza, Marie-Laure Potet, Stéphane Frénot, Valérie Viet Triem Tong, Nicolas Craipeau, Ronan Hardouin - Commun. ACM - [bibtex]
  3. Automated Proofs for Asymmetric Encryption. Judicaël Courant, Marion Daubignard, Cristian Ene, Pascal Lafourcade, Yassine Lakhnech - J. Autom. Reasoning - [bibtex]
  4. Runtime Enforcement Monitors: composition, synthesis, and enforcement abilities. Ylies Falcone, Jean-Claude Fernandez, Laurent Mounier, Jean-Luc Richier - Formal Methods in System Design - [bibtex]
  5. What can you Verify and Enforce at Runtime ? Ylies Falcone, Jean-Claude Fernandez, Laurent Mounier - Software Tool in Tecnology Transfer (STTT) - [bibtex]

2010

  1. Automata-based verification of programs with tree updates. Peter Habermehl, Radu Iosif, Tomás Vojnar - Acta Inf. - [bibtex]
  2. Quantitative Separation Logic and Programs with Lists. Marius Bozga, Radu Iosif, Swann Perarnau - J. Autom. Reasoning - [bibtex]
  3. Automatic Modular Abstractions for Template Numerical Constraints. David Monniaux - Logical Methods in Computer Science - PDF - [bibtex]

2009

  1. Convincing Proofs for Program Certification. Manuel Garnacho, Michaël Périn - Electronic Notes in Theoretical Computer Science - [bibtex]
  2. Flat Parametric Counter Automata. Marius Bozga, Radu Iosif, Yassine Lakhnech - Fundam. Inform. - [bibtex]
  3. A minimalistic look at widening operators. David Monniaux - Higher order and symbolic computation - PDF - [bibtex]

2008

  1. The pitfalls of verifying floating-point computations. David Monniaux - TOPLAS - [bibtex]

2006

  1. Tester la conformité d'un réseau à une politique de sécurité. Vianney Darmaillacq, Jean-Claude Fernandez, Roland Groz, Laurent Mounier, Jean-Luc Richier - Revue de l'electricité et de l'Electronique (REE) - [bibtex]
  2. Pattern-based abstraction for verifying secrecy in protocols. Liana Bozga, Yassine Lakhnech, Michaël Périn - International Journal on Software Tools for Technology Transfer (STTT) - [bibtex]

2005

  1. Translating Java for Multiple Model Checkers: The Bandera Back-End. Radu Iosif, Matthew B. Dwyer, John Hatcliff - Formal Methods in System Design - [bibtex]
  2. A symbolic decision procedure for cryptographic protocols with time stamps. Liana Bozga, Cristian Ene, Yassine Lakhnech - J. Log. Algebr. Program. - [bibtex]

2004

  1. Symmetry reductions for model checking of concurrent dynamic software. Radu Iosif - STTT - [bibtex]

2003

  1. Temporal logic properties of Java objects. Radu Iosif, Riccardo Sisto - Journal of Systems and Software - [bibtex]

2002

  1. Testing Theories for Broadcasting Processes. Cristian Ene, Traian Muntean - Sci. Ann. Cuza Univ. - [bibtex]

2000

  1. Verification and test generation for the SSCOP protocol. Marius Bozga, Jean-Claude Fernandez, Lucian Ghirvu, Claude Jard, Thierry Jéron, Alain Kerbrat, Pierre Morel, Laurent Mounier - Sci. Comput. Program - [bibtex]

1999

  1. A Deadlock Detection Tool for Concurrent Java Programs. Claudio Demartini, Radu Iosif, Riccardo Sisto - Softw., Pract. Exper. - [bibtex]

1998

  1. On Complexity of Reachability of Transition Restricted Petri Nets. Cristian Ene - Sci. Ann. Cuza Univ. - [bibtex]

1997

  1. Protocol Verification with the Aldebaran Toolset. Marius Bozga, Jean-Claude Fernandez, Alain Kerbrat, Laurent Mounier - Software Tools for Technology Transfer - [bibtex]
  2. Hierarchies of Petri Net Languages and a Super-Normal Form. Ferucio Laurentiu Tiplea, Cristian Ene - Journal of Automata, Languages and Combinatorics - [bibtex]

1996

  1. Specification and Verification of various Distributed Leader Election Algorithms for Unidirectional Ring Networks. Hubert Garavel, Laurent Mounier - Science of Computer Programming - [bibtex]

1994

  1. Some Decision Problems for Parallel Communicating Grammar Systems. Ferucio Laurentiu Tiplea, Cristian Ene, Cecilia Magdalena Ionescu, Octavian Procopiuc - Theor. Comput. Sci. - [bibtex]

1993

  1. A Coverability Structure for Parallel Communicating Grammar Systems. Ferucio Laurentiu Tiplea, Cristian Ene - Elektronische Informationsverarbeitung und Kybernetik - [bibtex]

1992

  1. On-the-Fly Verification of Finite Transition Systems. Jean-Claude Fernandez, Laurent Mounier, Claude Jard, Thierry Jéron - Formal Methods in System Design - [bibtex]

Book Chapters

2009

  1. Relaxing Restrictions on Invariant Composition in the B method by Spec# ownership control à la Spec#. Sylvain Boulmé, Marie-Laure Potet - Rigorous Methods for Software Construction and Analysis - [bibtex]

2008

  1. Modeling and Verification of Real Time Systems Using the IF Toolbox. Marius Bozga, Susanne Graf, Laurent Mounier, Iulian Ober - Real Time Systems 1: Modeling and verification techniques - [bibtex]

2006

  1. La boîte à outils IF pour la modélisation et la vérification de systèmes temps réel. Marius Bozga, Susanne Graf, Laurent Mounier, Iulian Ober - Systèmes temps réel : techniques de description et de vérification - [bibtex]

Conference Articles

2016

  1. Formal Analysis of Security Properties on the OPC-UA SCADA Protocol. Maxime Puys, Marie-Laure Potet, Pascal Lafourcade - International Conference on Computer Safety, Reliability, and Security (SAFECOMP'16) - [bibtex]
  2. Private Multi-party Matrix Multiplication and Trust Computations. Jean-Guillaume Dumas, Pascal Lafourcade, Jean-Baptiste Orfila, Maxime Puys - SECRYPT 2016 : 13th International Conference on Security and Cryptography - [bibtex]
  3. Domain Specific Stateful Filtering with Worst-Case Bandwidth. Maxime Puys, Jean-Louis Roch, Marie-Laure Potet - 11th International Conference on Critical Information Infrastructures Security (CRITIS 2016) - [bibtex]
  4. When the worst-case execution time estimation gains from the application semantics. Armelle Bonenfant, Fabienne Carrier, Hugues Cass'e, Philippe Cuenot, Denis Claraz, Nicolas Halbwachs, Hanbing Li, Claire Maiza, Marianne De Michiel, Vincent Mussot, Catherine Parent-Vigouroux, Isabelle Puaut, Pascal Raymond, Erven Rohou, Pascal Sotin - 8th European Congress on Embedded Real-Time Software and Systems - PDF - [bibtex]
  5. Finding the Needle in the Heap: Combining Static Analysis and Dynamic Symbolic Execution to Trigger Use-After-Free. Feist Josselin, Mounier Laurent, Marie-Laure Potet, Sebastien Bardin, David Robin - Proceedings of the 6th Software Security, Protection, and Reverse Engineering Workshop, SSPREW 2016, Los Angeles, USA, December 5-6, 2016 - [bibtex]
  6. FISSC: A Fault Injection and Simulation Secure Collection. Louis Dureuil, Guillaume Petiot, Marie-Laure Potet, Thanh-Ha Lee, Aude Crohen, Philippe De Choudens - Computer Safety, Reliability, and Security - 35th International Conference, SAFECOMP 2016, Trondheim, Norway, September 21-23, 2016, Proceedings - [bibtex]
  7. Specification of concretization and symbolization policies in symbolic execution. Robin David, Sebastien Bardin, Josselin Feist, Laurent Mounier, Marie-Laure Potet, Thanh Dinh Ta, Jean-Yves Marion - Proceedings of the 25th International Symposium on Software Testing and Analysis, ISSTA 2016, Saarbrucken, Germany, July 18-20, 2016 - [bibtex]
  8. Polyhedral Approximation of Multivariate Polynomials Using Handelman's Theorem. Alexandre Maréchal, Alexis Fouilhé, Tim King, David Monniaux, Michaël Périn - Verification, Model Checking, and Abstract Interpretation (VMCAI) - [bibtex]
  9. Formula Slicing: Inductive Invariants from Preconditions. Egor George Karpenkov, David Monniaux - Hardware and Software: Verification and Testing (Haifa Verification Conference) - [bibtex]
  10. Model Checking of Cache for WCET Analysis Refinement. Valentin Touzeau, Claire Maiza, David Monniaux - 10th Junior Researcher Workshop on Real-Time Computing - [bibtex]
  11. A Survey of Satisfiability Modulo Theory. David Monniaux - Computer Algebra in Scientific Computing - [bibtex]
  12. Cell Morphing: From Array Programs to Array-Free Horn Clauses. David Monniaux, Laure Gonnord - Static analysis - [bibtex]
  13. A Framework for Certified Self-Stabilization. Karine Altisen, Corbineau Pierre, Stéphane Devismes - FORTE'2016, the 36th IFIP International Conference on Formal Techniques for Distributed Objects, Components and System - [bibtex]
  14. BINSEC/SE: A Dynamic Symbolic Execution Toolkit for Binary-level Analysis. Robin David, Sebastien Bardin, Josselin Feist, Jean-Yves Marion, Marie-Laure Potet, Thanh Dinh Ta - Proceedings of SANER 2016 - [bibtex]
  15. Toward large-scale vulnerability discovery using Machine Learning. Gustavo Grieco, Guillermo Luis Grinblat, Lucas Uzal, Sanjay Rawat, Josselin Feist, Laurent Mounier - Proceedings of CODASPY 2016 publisher = ACM - [bibtex]
  16. Program Analysis with Local Policy Iteration. Egor George Karpenkov, David Monniaux, Philipp Wendler - Verification, Model Checking, and Abstract Interpretation (VMCAI) - [bibtex]

2015

  1. Performance Evaluations of Cryptographic Protocols. Verification Tools Dealing with Algebraic Properties. Pascal Lafourcade, Maxime Puys - To appear in FPS 2015 - [bibtex]
  2. A simple abstraction of arrays and maps by program translation. David Monniaux, Francesco Alberti - Static analysis (SAS) - [bibtex]
  3. Synthesis of ranking functions using extremal counterexamples. Laure Gonnord, David Monniaux, Gabriel Radanne - Programming Language Design and Implementation (PLDI) - [bibtex]
  4. Polyhedra to the rescue of array interpolants. Francesco Alberti, David Monniaux - ACM Symposium on Applied Computing, software verification and testing track - [bibtex]
  5. Lightweight Heuristics to Retrieve Parameter Associations from Binaries. Franck de Goer, Roland Groz, Laurent Mounier - Proceedings of the 5th Program Protection and Reverse Engineering Workshop - [bibtex]
  6. From Code Review to Fault Injection Attacks: Filling the Gap using Fault Model Inference). Louis Dureuil, Marie-Laure Potet, Philippe de Choudens, Cécile Dumas, Jessy Clediére - 14th Smart Card Research and Advanced Application Conference) - [bibtex]
  7. Refinement to Certify Abstract Interpretations, Illustrated on Linearization for Polyhedra. Sylvain Boulmé, Alexandre Maréchal - Interactive Theorem Proving - 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings - [bibtex]

2014

  1. High-Level Simulation for Multiple Fault Injection Evaluation. Maxime Puys, Lionel Rivi`ere, Julien Bringer, Thanh-Ha Le - Data Privacy Management, Autonomous Spontaneous Security, and Security Assurance - 9th International Workshop, DPM 2014, 7th International Workshop, SETOP 2014, and 3rd International Workshop, QA - [bibtex]
  2. On the Expressiveness of some Runtime Validation Techniques. Ylies Falcone, Jean-Claude Fernandez, Laurent Mounier - HOWARD-60: A Festschrift on the Occasion of Howard Barringer's 60th Birthday - [bibtex]
  3. Speeding Up Logico-Numerical Strategy Iteration. David Monniaux, Peter Schrammel - Static Analysis - 21st International Symposium, SAS 2014, Munich, Germany, September 11-13, 2014. Proceedings - [bibtex]
  4. Combining High-Level and Low-Level Approaches to Evaluate Software Implementations Robustness Against Multiple Fault Injection Attacks. Lionel Rivi`ere, Marie-Laure Potet, Thanh-Ha Le, Julien Bringer, Herve Chabanne, Maxime Puys - Foundations and Practice of Security - 7th International Symposium, FPS 2014, Montreal, QC, Canada, November 3-5, 2014. Revised Selected Papers - [bibtex]
  5. How to compute worst-case execution time by optimization modulo theory and a clever encoding of program semantics. Julien Henry, Mihail Asavoae, David Monniaux, Claire Maiza - SIGPLAN/SIGBED Conference on Languages, Compilers and Tools for Embedded Systems 2014, LCTES '14 - [bibtex]
  6. LiSTT: An Investigation into Unsound-incomplete Yet Practical Result Yielding Static Taintflow Analysis. Sanjay Rawat, Laurent Mounier, Marie-Laure Potet - Proceedings of SAW 2014 (ARES Workshop) - [bibtex]
  7. Modular and lightweight certification of polyhedral abstract domains. Alexis Fouilhé, Sylvain Boulmé, Michaël Périn - Types for Proofs and Programs (TYPES 2014) -- Book of Abstracts - [bibtex]
  8. A certifying frontend for (sub)polyhedral abstract domains. Alexis Fouilhé, Sylvain Boulmé - Verified Software: Theories, Tools and Experiments (VSTTE 2014) - [bibtex]
  9. Safety Problems Are NP-complete for Flat Integer Programs with Octagonal Loops. Marius Bozga, Radu Iosif, Filip Konecn\'y - Verification, Model Checking, and Abstract Interpretation - 15th International Conference, VMCAI 2014, San Diego, CA, USA, January 19-21, 2014, Proceedings - [bibtex]
  10. Lazart: a symbolic approach for evaluation the robustness of secured codes against control flow fault injection. Marie-Laure Potet, Laurent Mounier, Maxime Puys, Louis Dureuil - ICST - [bibtex]

2013

  1. Efficient Generation of Correctness Certificates for the Abstract Domain of Polyhedra. Alexis Fouilhé, David Monniaux, Michaël Périn - Static analysis (SAS) - [bibtex]
  2. The Tree Width of Separation Logic with Recursive Definitions. Radu Iosif, Adam Rogalewicz, Jirí Simácek - Automated Deduction - CADE-24 - 24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013. Proceedings - [bibtex]
  3. Implementing hash-consed data structures in Coq. Thomas Braibant, Jacques-Henri Jourdan, David Monniaux - Interactive theorem proving (ITP) - [bibtex]
  4. Predictive Taint Analysis for Extended Testing of Parallel Executions. Emmanuel Sifakis, Laurent Mounier - Hardware and Software: Verification and Testing - 9th International Haifa Verification Conference - [bibtex]
  5. CIL Security Proof for a Password-Based Key Exchange. Cristian Ene, Clémentine Gritti, Yassine Lakhnech - Provable Security - 7th International Conference, ProvSec 2013, Melaka, Malaysia, October 23-25, 2013. Proceedings - [bibtex]
  6. On Unique Decomposition of Processes in the Applied -Calculus. Jannik Dreier, Cristian Ene, Pascal Lafourcade, Yassine Lakhnech - Foundations of Software Science and Computation Structures - 16th International Conference, FOSSACS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, - [bibtex]
  7. A stack model for symbolic buffer overflow exploitability analysis (Extended Abstract). Gustavo Grieco, Laurent Mounier, Marie-Laure Potet, Sanjay Rawat - 5th Workshop on the Constraints in Software Testing, Verification and Analysis CSTVA 2013 (in association with ICST 2013) - [bibtex]
  8. Underapproximation of Procedure Summaries for Integer Programs. Pierre Ganty, Radu Iosif, Filip Konecn\'y - TACAS - [bibtex]

2012

  1. A Taint Based Approach for Smart Fuzzing. Sofia Bekrar, Chaouki Bekrar, Roland Groz, Laurent Mounier - Proceedings of SecTest - [bibtex]
  2. Dynamic Information-Flow Analysis for Multi-threaded Applications. Laurent Mounier, Emmanuel Sifakis - Proceedings of ISoLA - [bibtex]
  3. Finding Buffer Overflow Inducing Loops in Binary Executables. Sanjay Rawat, Laurent Mounier - Proceedings of Sixth International Conference on Software Security and Reliability (SERE) - [bibtex]
  4. Accelerating Interpolants. Hossein Hojjat, Radu Iosif, Filip Konecn\'y, Viktor Kuncak, Philipp Rümmer - ATVA - [bibtex]
  5. A Verification Toolkit for Numerical Transition Systems - Tool Paper. Hossein Hojjat, Filip Konecn\'y, Florent Garnier, Radu Iosif, Viktor Kuncak, Philipp Rümmer - FM - [bibtex]
  6. Succinct Representations for Abstract Interpretation. Julien Henry, David Monniaux, Matthieu Moy - Static analysis (SAS) - [bibtex]
  7. PAGAI: a path sensitive static analyzer. Julien Henry, David Monniaux, Matthieu Moy - Tools for Automatic Program Analysis (TAPAS) - [bibtex]
  8. Anatomy of Alternating Quantifier Satisfiability (Work in progress). Anh-Dung Phan, Nikolaj Bj\orner, David Monniaux - 10th International Workshop on Satisfiability Modulo Theories (SMT) - [bibtex]
  9. Experiments on the feasibility of using a floating-point simplex in an SMT solver. Diego Caminha Barbosa de Oliveira, David Monniaux - Workshop on Practical Aspects of Automated Reasoning (PAAR) - [bibtex]
  10. Deciding Conditional Termination. Marius Bozga, Radu Iosif, Filip Konecn\'y - Tools and Algorithms for the Construction and Analysis of Systems - 18th International Conference, TACAS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS - [bibtex]

2011

  1. Politiques de gestion de protections pour l'implémentation de sections critiques.. Sifakis Emmanuel, Mounier Laurent - Actes des Rencontres du Parallélisme (RenPar) - [bibtex]
  2. Définition des responsabilités pour les dysfonctionnements de logiciels : cadre contractuel et outils de mise en oeuvre.. Sylvain Steer, Nicolas Craipeau, Daniel Le Métayer, Manuel Maareck, Marie-Laure Potet, Valérie Viet Triem Tong - Droit, sciences et techniques : quelles responsabilités ? colloque international du Réseau Droit, sciences et techniques. - [bibtex]
  3. Certified Security Proofs of Cryptographic Protocols in the Computational Model: An Application to Intrusion Resilience. Pierre Corbineau, Mathilde Duclos, Yassine Lakhnech - Certified Programs and Proofs - First International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings - [bibtex]
  4. Finding Software Vulnerabilities by Smart Fuzzing. Sofia Bekrar, Chaouki Bekrar, Roland Groz, Laurent Mounier - IEEE Fourth International Conference on Software Testing, Verification and Validation, ICST 2011, Berlin, Germany, 21-25 March 2011 - [bibtex]
  5. On the Generation of Positivstellensatz Witnesses in Degenerate Cases. David Monniaux, Pierre Corbineau - Interactive Theorem Proving (ITP) - PDF - [bibtex]
  6. Modular Abstractions of Reactive Nodes using Disjunctive Invariants. David Monniaux, Martin Bodin - Programming Languages and Systems (APLAS) - PDF - [bibtex]
  7. Stratified Static Analysis Based on Variable Dependencies. David Monniaux, Julien Le Guen - Third International Workshop on Numerical and Symbolic Abstract Domains - PDF - [bibtex]
  8. Using bounded model checking to focus fixpoint iterations. David Monniaux, Laure Gonnord - Static analysis (SAS) - PDF - [bibtex]
  9. Designing a CPU model: from a pseudo-formal document to fast code. Frédéric Blanqui, Claude Helmstetter, Vania Joloboff, Jean-François Monin, Xiaomu Shi - Proceedings of the 3rd Workshop on Rapid Simulation and Performance Evaluation: Methods and Tools - [bibtex]
  10. A refinement methodology for object-oriented programs. Asma Tafat, Sylvain Boulmé, Claude Marché - Formal Verification of Object-Oriented Software - [bibtex]
  11. Offset-Aware Mutation based Fuzzing for Buffer Overflow Vulnerabilities: Few Preliminary Results. Sanjay Rawat, Laurent Mounier - Proc. of The Second International Workshop on Security Testing (SECTEST) - PDF - [bibtex]
  12. Improving Strategies via SMT Solving. Thomas Gawlitza, David Monniaux - ESOP - PDF - [bibtex]
  13. Synchronous Programming of Device Drivers for Global Resource Control in Embedded Operating Systems. Nicolas Berthier, Florence Maraninchi, Laurent Mounier - ACM SIGPLAN/SIGBED Conference on Languages, Compilers, Tools and Theory for Embedded Systems (LCTES) - [bibtex]

2010

  1. Fast Acceleration of Ultimately Periodic Relations. Marius Bozga, Radu Iosif, Filip Konecn\'y - Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings - [bibtex]
  2. Automated Proofs for Asymmetric Encryption. Judicaël Courant, Marion Daubignard, Cristian Ene, Pascal Lafourcade, Yassine Lakhnech - Concurrency, Compositionality, and Correctness, Essays in Honor of Willem-Paul de Roever - [bibtex]
  3. Quantifier elimination by lazy model enumeration. David Monniaux - Computer-aided verification (CAV) - PDF - [bibtex]
  4. Proof Trick: Small Inversions. Jean-François Monin - Second Coq Workshop - [bibtex]
  5. A Formal Framework for Specifying and Analyzing Logs as Electronic Evidence. Eduardo Mazza, Marie-Laure Potet, Daniel Le Métayer - 13th Brazilian Symposium of Formal Methods (SBMF) - [bibtex]
  6. An Evolutionary Computing Approach for Hunting Buffer Overflow Vulnerabilities: A case of aiming in dim light. Sanjay Rawat, Laurent Mounier - Proceedings of 6th EC2ND (European Conference on Computer Network Defense - [bibtex]
  7. More Testable Properties. Ylies Falcone, Jean-Claude Fernandez, Thierry Jéron, Hervé Marchand, Laurent Mounier - Proceedings of ICTSS - 22nd IFIP WG 6.1 International Conference - PDF - [bibtex]
  8. Designing Log Architecture For Legal Evidence. Daniel Le Métayer, Eduardo Mazza, Marie-Laure Potet - Software Engineering And Formal Methods (SEFM) - [bibtex]
  9. Taint Dependency Sequences: A Characterization of Insecure Execution Paths Based on Input-Sensitive Cause Sequences. Dumitru Ceara, Laurent Mounier, Marie-Laure Potet - ICSTW '10: Proceedings of the 2010 Third International Conference on Software Testing, Verification, and Validation Workshops - [bibtex]
  10. Liability in software Engineering. Daniel Le Métayer, Manuel Maarek, Eduardo Mazza, Marie-Laure Potet, Stéphane Frénot, Valérie Viet Triem Tong, Nicolas Craipeau, Ronan Hardouin - ICSE 2010, International Conference on Software Engineering - [bibtex]

2009

  1. Automata-Based Termination Proofs. Radu Iosif, Adam Rogalewicz - Implementation and Application of Automata, 14th International Conference, CIAA 2009, Sydney, Australia, July 14-17, 2009. Proceedings - [bibtex]
  2. Formal Indistinguishability Extended to the Random Oracle Model. Cristian Ene, Yassine Lakhnech, Van Chan Ngo - Computer Security - ESORICS 2009, 14th European Symposium on Research in Computer Security, Saint-Malo, France, September 21-23, 2009. Proceedings - [bibtex]
  3. "Certfication of Smart-Card Applications in Common Criteria". Iman Narasamdya, Michaël Périn - ACM Symposium on Applied Computing - [bibtex]
  4. "Certfication of Smart-Card Applications in Common Criteria: Proving Representation Correspondences". Iman Narasamdya, Michaël Périn - Fundamental Approaches to Software Engineering - [bibtex]
  5. Automatic Verification of Integer Array Programs. Marius Bozga, Peter Habermehl, Radu Iosif, Filip Konecn\'y, Tomás Vojnar - Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings - [bibtex]
  6. Iterating Octagons. Marius Bozga, Codruta G\^\irlea, Radu Iosif - Tools and Algorithms for the Construction and Analysis of Systems, 15th International Conference, TACAS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2 - [bibtex]
  7. Automatic Modular Abstractions for Linear Constraints. David Monniaux - POPL (Principles of programming languages) - PDF - [bibtex]
  8. On using floating-point computations to help an exact linear arithmetic decision procedure. David Monniaux - Computer-aided verification (CAV) - PDF - [bibtex]
  9. Invariants and Robustness of BIP Models. Jan Olaf Blech, Thanh-Hung Nguyen, Michaël Périn - Workshop on Invariant Generation (WING) - [bibtex]
  10. Certifying Deadlock-freedom for BIP Models. Jan Olaf Blech, Michaël Périn - Software and Compilers for Embedded Systems (SCOPES) - [bibtex]
  11. Runtime Verification of Safety Progress Properties. Ylies Falcone, Jean-Claude Fernandez, Laurent Mounier - Runtime Verification 2009 - [bibtex]
  12. Enforcement Monitoring wrt. the Safety-Progress Classification of Properties. Ylies Falcone, Jean-Claude Fernandez, Laurent Mounier - Proceedings of the 24th Annual ACM Symposium on Applied Computing - Software Verification and Testing Track - [bibtex]

2008

  1. A New Elimination Rule for the Calculus of Inductive Constructions. Bruno Barras, Pierre Corbineau, Benjamin Grégoire, Hugo Herbelin, Jorge Luis Sacchini - Types for Proofs and Programs (International Conference TYPES 2008, Revised Selected Papers) - [bibtex]
  2. A Logic of Singly Indexed Arrays. Peter Habermehl, Radu Iosif, Tomás Vojnar - Logic for Programming, Artificial Intelligence, and Reasoning, 15th International Conference, LPAR 2008, Doha, Qatar, November 22-27, 2008. Proceedings - [bibtex]
  3. Towards automated proofs for asymmetric encryption schemes in the random oracle model. Judicaël Courant, Marion Daubignard, Cristian Ene, Pascal Lafourcade, Yassine Lakhnech - Proceedings of the 2008 ACM Conference on Computer and Communications Security, CCS 2008, Alexandria, Virginia, USA, October 27-31, 2008 - [bibtex]
  4. Quantitative Separation Logic and Programs with Lists. Marius Bozga, Radu Iosif, Swann Perarnau - Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings - [bibtex]
  5. What Else Is Decidable about Integer Arrays? Peter Habermehl, Radu Iosif, Tomás Vojnar - Foundations of Software Science and Computational Structures, 11th International Conference, FOSSACS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008 - [bibtex]
  6. A Quantifier Elimination Algorithm for Linear Real Arithmetic. David Monniaux - LPAR (Logic for Programming Artificial Intelligence and Reasoning) - PDF - [bibtex]
  7. Combination of Abstractions in the ASTRÉE Static Analyzer. Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, Xavier Rival - Advances in Computer Science --- ASIAN 2006. Secure Software and Related Issues - [bibtex]
  8. A B Formal Framework for Security Developments in the Domain of Smart Card Applications. Frédéric Dadeau, Marie-Laure Potet, Régis Tissot - SEC'2008, 23rd int. Information Security Conference - [bibtex]
  9. A Verifiable Conformance Relationship between Smart Card Applets and B Models. Frédéric Dadeau, Julien Lamboley, Thierry Moutet, Marie-Laure Potet - ABZ'2008, International Conference on ASM, B and Z - [bibtex]
  10. Automated Proofs for Asymmetric Encryption. Judicaël Courant, Marion Daubignard, Cristian Ene, Pascal Lafourcade, Yassine Lakhnech - Proceedings of the LICS-Affiliated Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis - [bibtex]
  11. A Model Transformation Tool for Performance Simulation of Complex UML Models. Olivier Constant, Wei Monin, Susanne Graf - ICSE 2008, tool track - [bibtex]
  12. j-POST: a Java Toolchain for Property-Oriented Software Testing. Ylies Falcone, Laurent Mounier, Jean-Claude Fernandez, Jean-Luc Richier - Model-Based Testing (MBT) - [bibtex]
  13. Synthesizing Enforcement Monitors wrt. the Safety-Progress Classification of Properties. Ylies Falcone, Jean-Claude Fernandez, Laurent Mounier - International Conference of Information System Security - [bibtex]

2007

  1. Using BIP for Modeling and Verification of Networked Systems - A Case Study on TinyOS-based Networks. Ananda Basu, Laurent Mounier, Marc Poulhiès, Jacques Pulou, Joseph Sifakis - IEEE NCA'07 - [bibtex]
  2. Using BIP for Modeling and Verification of Networked Systems -- A Case Study on TinyOS-based Networks. Ananda Basu, Laurent Mounier, Marc Poulhiès, Jacques Pulou, Joseph Sifakis - Sixth IEEE International Symposium on Network Computing and Applications (NCA 2007), 12 - 14 July 2007, Cambridge, MA, USA - [bibtex]
  3. On Flat Programs with Lists. Marius Bozga, Radu Iosif - Verification, Model Checking, and Abstract Interpretation, 8th International Conference, VMCAI 2007, Nice, France, January 14-16, 2007, Proceedings - [bibtex]
  4. Proving Termination of Tree Manipulating Programs. Peter Habermehl, Radu Iosif, Adam Rogalewicz, Tomás Vojnar - Automated Technology for Verification and Analysis, 5th International Symposium, ATVA 2007, Tokyo, Japan, October 22-25, 2007, Proceedings - [bibtex]
  5. Intuitionistic Refinement Calculus.. Sylvain Boulmé - Typed Lambda Calculi and Applications - PDF - [bibtex]
  6. Interpreting invariant composition in the B method using the Spec\# ownership relation: a way to explain and relax B restrictions. Sylvain Boulmé, Marie-Laure Potet - B 2007 - [bibtex]
  7. Test Generation from Security Policies Specified in Or-BAC. Keqin Li, Laurent Mounier, Roland Groz - IEEE COMPSAC'07 - [bibtex]
  8. Verification of Device Drivers and Intelligent Controllers: a Case Study. David Monniaux - EMSOFT - [bibtex]
  9. Worst-case lifetime computation of a Wireless Sensor Network by model-checking. Laurent Mounier, Ludovic Samper, Wassim Znaidi - Fourth ACM Workshop on Performance Evaluation of Wireless Ad Hoc, Sensor, and Ubiquitous Networks (PE-WASUN) - [bibtex]
  10. The ARESA Project: Facilitating Research, Development and Commercialization of WSNs. Mischa Dohler, Dominique Barthel, Florence Maraninchi, Laurent Mounier, Stéphane Aubert, Christophe Dugas, Aurélien Buhrig, Franck Paugnat, Marc Renaudin, Andrzej Duda, Martin Heusse, Fabrice Valois - IEEE SECON'07 (Fourth Annual IEEE Communications Society Conference on Sensor, Mesh and Ad Hoc Communications and Networks) - [bibtex]
  11. Computationally Sound Typing for Non-interference: The Case of Deterministic Encryption. Judicaël Courant, Cristian Ene, Yassine Lakhnech - FSTTCS 2007: Foundations of Software Technology and Theoretical Computer Science, 27th International Conference, New Delhi, India, December 12-14, 2007, Proceedings - [bibtex]
  12. A Compositional Testing Framework Driven by Partial Specifications. Ylies Falcone, Jean-Claude Fernandez, Laurent Mounier, Jean-Luc Richier - TESTCOM/FATES - [bibtex]

2006

  1. Automata-Based Verification of Programs with Tree Updates. Peter Habermehl, Radu Iosif, Tomás Vojnar - Tools and Algorithms for the Construction and Analysis of Systems, 12th International Conference, TACAS 2006 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 20 - [bibtex]
  2. Programs with Lists Are Counter Automata. Ahmed Bouajjani, Marius Bozga, Peter Habermehl, Radu Iosif, Pierre Moro, Tomás Vojnar - Computer Aided Verification, 18th International Conference, CAV 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings - [bibtex]
  3. Flat Parametric Counter Automata. Marius Bozga, Radu Iosif, Yassine Lakhnech - Automata, Languages and Programming, 33rd International Colloquium, ICALP 2006, Venice, Italy, July 10-14, 2006, Proceedings, Part II - [bibtex]
  4. Test Generation for Network Security Rules. Vianney Darmaillacq, Jean-Claude Fernandez, Roland Groz, Laurent Mounier, Jean-Luc Richier - TestCom'06 - [bibtex]
  5. A Test Calculus Framework Applied to Network Security Policies. Ylies Falcone, Jean-Claude Fernandez, Laurent Mounier, Jean-Luc Richier - FATES/RV'06 - [bibtex]
  6. GLONEMO: Global and Accurate Formal Models for the Analysis of Ad-Hoc Sensor Networks. Ludovic Samper, Florence Maraninchi, Laurent Mounier, Louis Mandel - InterSense: First International Conference on Integrated Internet Ad hoc and Sensor Networks - [bibtex]
  7. Certification of Cryptographic Protocols by Abstract Model-Checking and Proof Concretization. Romain Janvier, Yassine Lakhnech, Michaël Périn - Workshop on Innovative Techniques for the Certification of Embedded Systems On the Importance of Modeling the Environment when Analyzing Sensor Networks. Ludovic Samper, Florence Maraninchi, Laurent Mounier, Erwan Jahier, Pascal Raymond - 3rd International Workshop on Wireless Ad-hoc and Sensor Networks (IWWAN'06) - [bibtex]
  8. Confirmation of Deadlock Potentials Detected by Runtime Analysis. Saddek Bensalem, Jean-Claude Fernandez, Klaus Havelund, Laurent Mounier - Parallel and Distributed Systems: Testing and Debugging 2006 (PADTAD'06) - [bibtex]
  9. Qualification d'architectures fontionnelles. Marius Bozga, Pierre Combes, Susanne Graf, Wei Monin, Nicolas Moteau - Notere'06 - [bibtex]

2005

  1. On Decidability Within the Arithmetic of Addition and Divisibility. Marius Bozga, Radu Iosif - Foundations of Software Science and Computational Structures, 8th International Conference, FOSSACS 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, - [bibtex]
  2. Eléments de modélisation pour le test de politiques de sécurité. Vianney Darmaillacq, Jean-Claude Fernandez, Roland Groz, Laurent Mounier, Jean-Luc Richier - Colloque sur les RIsques et la Sécurité d'Internet et des Systèmes, CRiSIS - [bibtex]
  3. Automatic Verification of Security Properties Based on Abstractions. Liana Bozga, Cristian Ene, Romain Janvier, Yassine Lakhnech, Laurent Mazaré, Michaël Périn - Proceedings of the NATO Advanced Research Workshop Verification of Infinite State Systems with Applications to Security VISS - [bibtex]
  4. A model-based approach for robustness testing. Jean-Claude Fernandez, Laurent Mounier, Cyril Pachon - TestCom 2005 - [bibtex]

2004

  1. On Logics of Aliasing. Marius Bozga, Radu Iosif, Yassine Lakhnech - Static Analysis, 11th International Symposium, SAS 2004, Verona, Italy, August 26-28, 2004, Proceedings - [bibtex]
  2. On the Existence of an Effective and Complete Inference System for Cryptographic Protocols. Liana Bozga, Cristian Ene, Yassine Lakhnech - Foundations of Software Science and Computation Structures, 7th International Conference, FOSSACS 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, B - [bibtex]
  3. A symbolic decision procedure for bounded security protocols with time stamps (Extended abstract). Liana Bozga, Cristian Ene, Yassine Lakhnech - CONCUR 2004 - Concurrency Theory, 15th International Conference, London, UK, August 31 - September 3, 2004, Proceedings - [bibtex]
  4. IF Tutorial. Marius Bozga, Susanne Graf, Laurent Mounier, Iulian Ober - 9th SPIN'04 Workshop on Model-Checking of Software, Barcelona, Spain - [bibtex]
  5. A Symbolic Decision Procedure for Cryptographic Protocols with Time Stamps (Extended Abstract). Liana Bozga, Cristian Ene, Yassine Lakhnech - CONCUR 2004 - Concurrency Theory, 15th International Conference, London, UK, August 31 - September 3, 2004, Proceedings - [bibtex]

2003

  1. Storeless semantics and alias logic. Marius Bozga, Radu Iosif, Yassine Lakhnech - Proceedings of the 2003 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-based Program Manipulation, 2003, San Diego, California, USA, June 7, 2003 - [bibtex]
  2. Pattern-Based Abstraction for Verifying Secrecy in Protocols. Liana Bozga, Yassine Lakhnech, Michaël Périn - Tools and Algorithms for the Construction and Analysis of Systems, 9th International Conference, TACAS 2003, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 20 - [bibtex]
  3. Abstract Interpretation for Secrecy using Patterns. Liana Bozga, Yassine Lakhnech, Michaël Périn - TACAS'03 - [bibtex]
  4. HERMES: An Automatic Tool for Verification of Secrecy in Security Protocols. Liana Bozga, Yassine Lakhnech, Michaël Périn - 15th International Conference on Computer Aided Verification (CAV), - [bibtex]
  5. Validation of asynchronous circuit specifications using IF/CADP. Dominique Borrione, Menouer Boubekeur, Laurent Mounier, Marc Renaudin, Antoine Sirianni - IFIP Intl. Conference on VLSI, Darmstadt, Germany - [bibtex]
  6. Modelling CHP descriptions in Labelled Transition Systems for an efficient formal validations of asynchronous circuit specifications. Menouer Boubekeur, Dominique Borrione, Laurent Mounier, Marc Renaudin, Antoine Sirianni - Forum on Specification and Design Language (FDL'03), Frankfurt, Germany - [bibtex]
  7. Property Oriented Test Case Generation. Jean-Claude Fernandez, Laurent Mounier, Cyril Pachon - Proceedings of FATES'03 (Satellite workshop of ASE'03), Montreal, Canada - [bibtex]

2002

  1. Symmetry Reduction Criteria for Software Model Checking. Radu Iosif - Model Checking of Software, 9th International SPIN Workshop, Grenoble, France, April 11-13, 2002, Proceedings - [bibtex]
  2. IF-2.0: A Validation Environment for Component-Based Real-Time Systems. Marius Bozga, Susanne Graf, Laurent Mounier - Proceedings of Conference on Computer Aided Verification, CAV'02, Copenhagen - [bibtex]

2001

  1. Temporal Logic Properties of Java Objects. Radu Iosif, Riccardo Sisto - Proceedings of the Thirteenth International Conference on Software Engineering & Knowledge Engineering (SEKE'2001), Sheraton Buenos Aires Hotel, Buenos Aires, Argentina, June 13-15, 2001 - [bibtex]
  2. Exploiting Heap Symmetries in Explicit-State Model Checking of Software. Radu Iosif - 16th IEEE International Conference on Automated Software Engineering (ASE 2001), 26-29 November 2001, Coronado Island, San Diego, CA, USA - [bibtex]
  3. Automated validation of distributed software using the IF environment. Marius Bozga, Laurent Mounier, Susanne Graf - 2001 IEEE International Symposium on Network Computing and Applications (NCA 2001) - [bibtex]
  4. Model-Checking Ariane-5 Flight Program. Marius Bozga, David Lesens, Laurent Mounier - Proceedings of FMICS'01 (Paris, France) - [bibtex]
  5. Automated validation of distributed software using the IF environment. Marius Bozga, Susanne Graf, Laurent Mounier - Workshop on Software Model-checking, associated with CAV 2001, Paris - [bibtex]
  6. Timed Extensions for SDL. Marius Bozga, Alain Kerbrat, Susanne Graf, Laurent Mounier, Iulian Ober, Daniel Vincent - Proceedings of SDL FORUM'01 (Copenhagen, Denmark) - [bibtex]
  7. A Broadcast-based Calculus for Communicating Systems. Cristian Ene, Traian Muntean - Proceedings of the 15th International Parallel & Distributed Processing Symposium (IPDPS-01), San Francisco, CA, April 23-27, 2001 - [bibtex]

2000

  1. Using Garbage Collection in Model Checking. Radu Iosif, Riccardo Sisto - SPIN Model Checking and Software Verification, 7th International SPIN Workshop, Stanford, CA, USA, August 30 - September 1, 2000, Proceedings - [bibtex]
  2. Formal verification applied to Java concurrent software. Radu Iosif - Proceedings of the 22nd International Conference on on Software Engineering, ICSE 2000, Limerick Ireland, June 4-11, 2000 - [bibtex]
  3. IF: A Validation Environment for Timed Asynchronous Systems. Marius Bozga, Lucian Ghirvu, Susanne Graf, Laurent Mounier - Proceedings of Conference on Computer Aided Verification, CAV'00, Chicago - [bibtex]
  4. SDL for Real Time: What is missing? Marius Bozga, Susanne Graf, Alain Kerbrat, Laurent Mounier, Iulian Ober, Daniel Vincent - Proceedings of SAM'00: 2nd Workshop on SDL and MSC (Grenoble, France) - [bibtex]
  5. Compositional State Space Generation with Partial Order Reductions for Asynchronous Communicating Systems. Jean-Pierre Krimm, Laurent Mounier - Proceedings of TACAS'00 - [bibtex]

1999

  1. dSPIN: A Dynamic Extension of SPIN. Claudio Demartini, Radu Iosif, Riccardo Sisto - Theoretical and Practical Aspects of SPIN Model Checking, 5th and 6th International SPIN Workshops, Trento, Italy, July 5, 1999, Toulouse, France, September 21 and 24 1999, Proceedings - [bibtex]
  2. IF: An Intermediate Representation and Validation Environment for Timed Asynchronous Systems. Marius Bozga, Jean-Claude Fernandez, Lucian Ghirvu, Susanne Graf, Jean-Pierre Krimm, Laurent Mounier - Proceedings of Symposium on Formal Methods 99, Toulouse - [bibtex]
  3. IF: An Intermediate Representation for SDL and its Applications. Marius Bozga, Jean-Claude Fernandez, Lucian Ghirvu, Susanne Graf, Jean-Pierre Krimm, Laurent Mounier, Joseph Sifakis - Proceedings of SDL Forum 99, Montreal - [bibtex]
  4. Expressiveness of Point-to-Point versus Broadcast Communications. Cristian Ene, Traian Muntean - Fundamentals of Computation Theory, 12th International Symposium, FCT '99, Iasi, Romania, August 30 - September 3, 1999, Proceedings - [bibtex]

1997

  1. Compositional State Space Generation from Lotos Programs. Jean-Pierre Krimm, Laurent Mounier - Proceedings of TACAS'97 (Tools and Algorithms for the Construction and Analysis of Systems), Enschede, The Netherlands - [bibtex]

1996

  1. CADP - A Protocol Validation and Verification Toolbox. Jean-Claude Fernandez, Hubert Garavel, Alain Kerbrat, Laurent Mounier, Radu Mateescu, Mihaela Sighireanu - Computer Aided Verification, 8th International Conference, CAV '96, New Brunswick, NJ, USA, July 31 - August 3, 1996, Proceedings - [bibtex]
  2. Specification and Verification of the PowerScale Bus Arbitration Protocol: An Industrial Experiment with LOTOS. Ghassan Chehaibar, Hubert Garavel, Laurent Mounier, Nadia Tawbi, Ferruccio Zulian - Proceedings of the Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols, and Protocol Specification, Testing, and Verification FORTE/PST - [bibtex]

1995

  1. Hierarchies of Petri Net Languages and a Super-Normal Form. Ferucio Laurentiu Tiplea, Cristian Ene - Developments in Language Theory - [bibtex]

1993

  1. Symbolic Equivalence Checking. Jean-Claude Fernandez, Alain Kerbrat, Laurent Mounier - Proceedings of the 5th Workshop on Computer-Aided Verification (Heraklion, Greece) - [bibtex]

1992

  1. A Toolbox for the Verification of LOTOS Programs. Jean-Claude Fernandez, Hubert Garavel, Laurent Mounier, Anne Rasse, Carlos Rodríguez, Joseph Sifakis - Proceedings of the 14th International Conference on Software Engineering ICSE'14 (Melbourne, Australia) - [bibtex]

PhD Thesis and HDR

2009

  1. Analyse statique : de la théorie à la pratique. David Monniaux - Habilitation to direct research - [bibtex]

1992

  1. Méthodes de Vérification de Spécifications Comportementales : étude et mise en oeuvre. Laurent Mounier - [bibtex]

Contact | Site Map | Site powered by SPIP 3.0.24 + AHUNTSIC [CC License]

info visites 729081