Skip to Main content
Number of documents

70

David Monniaux


Senior researcher at CNRS

Director of the VERIMAG laboratory


Journal articles15 documents

  • David Monniaux. The complexity gap in the static analysis of cache accesses grows if procedure calls are added. Formal Methods in System Design, Springer Verlag, In press, ⟨10.1007/s10703-022-00392-w⟩. ⟨hal-03545774⟩
  • David Monniaux, Cyril Six. Formally Verified Loop-Invariant Code Motion and Assorted Optimizations. ACM Transactions on Embedded Computing Systems (TECS), ACM, In press, ⟨10.1145/3529507⟩. ⟨hal-03628646⟩
  • Camille Coti, David Monniaux, Hang yu. A task-based approach to parallel parametric linear programming solving, and application to polyhedral computations. Concurrency and Computation: Practice and Experience, John Wiley & Sons Ltd, 2021, 33 (6), pp.e6050. ⟨10.1002/cpe.6050⟩. ⟨hal-02951016⟩
  • Cyril Six, Sylvain Boulmé, David Monniaux. Certified and efficient instruction scheduling. Application to interlocked VLIW processors.. Proceedings of the ACM on Programming Languages, ACM, 2020, OOPSLA 2020, pp.129. ⟨10.1145/3428197⟩. ⟨hal-02185883v3⟩
  • David Monniaux, Valentin Touzeau. On the complexity of cache analysis for different replacement policies. Journal of the ACM (JACM), Association for Computing Machinery, 2019, 66 (6), pp.41. ⟨10.1145/3366018⟩. ⟨hal-01910216v3⟩
  • Claire Maïza, Valentin Touzeau, David Monniaux, Jan Reineke. Fast and exact analysis for LRU caches. Proceedings of the ACM on Programming Languages, ACM, 2019, 3 (POPL), ⟨10.1145/3290367⟩. ⟨hal-01908648v2⟩
  • David Monniaux. On the decidability of the existence of polyhedral invariants in transition systems. Acta Informatica, Springer Verlag, 2019, 56 (4), pp.385-389. ⟨10.1007/s00236-018-0324-y⟩. ⟨hal-01587125v2⟩
  • Virginie Gautron, David Monniaux. De la surveillance secrète à la prédiction des risques : les dérives du fichage dans le champ de la lutte contre le terrorisme. Archives de politique criminelle, A. Pedone, 2016, Terrorismes, 38, pp.123-135. ⟨hal-01446359⟩
  • Thomas Braibant, Jacques-Henri Jourdan, David Monniaux. Implementing and reasoning about hash-consed data structures in Coq. Journal of Automated Reasoning, Springer Verlag, 2014, 53 (3), pp.271-304. ⟨10.1007/s10817-014-9306-0⟩. ⟨hal-00881085v4⟩
  • David Monniaux, Julien Le Guen. Stratified Static Analysis Based on Variable Dependencies. Electronic Notes in Theoretical Computer Science, Elsevier, 2012, Proceedings of the Third International Workshop on Numerical and Symbolic Abstract Domains, NSAD 2011, 288, pp.61-74. ⟨10.1016/j.entcs.2012.10.008⟩. ⟨hal-00622137⟩
  • David Monniaux. Initiation à la calculabilité. Quadrature, EDP Sciences, 2012, pp.17-28. ⟨hal-01446372⟩
  • David Monniaux. Automatic modular abstractions for template numerical constraints. Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2010, 6 (3), pp.4. ⟨10.2168/LMCS-6(3:4)2010⟩. ⟨hal-00418992v2⟩
  • David Monniaux. A minimalistic look at widening operators. Higher-Order and Symbolic Computation, Springer Verlag, 2009, 22 (2), pp.145-154. ⟨10.1007/s10990-009-9046-8⟩. ⟨hal-00363204v3⟩
  • David Monniaux. The pitfalls of verifying floating-point computations. ACM Transactions on Programming Languages and Systems (TOPLAS), ACM, 2008, 30 (3), pp.12. ⟨10.1145/1353445.1353446⟩. ⟨hal-00128124v5⟩
  • David Monniaux. Abstract interpretation of programs as Markov decision processes. Science of Computer Programming, Elsevier, 2005, 58, pp.179-205. ⟨10.1016/j.scico.2005.02.008⟩. ⟨hal-00084297⟩

Conference papers43 documents

  • Cyril Six, Léo Gourdin, Sylvain Boulmé, David Monniaux, Justus Fasse, et al.. Formally Verified Superblock Scheduling. Certified Programs and Proofs (CPP ’22), Jan 2022, Philadelphia, United States. ⟨10.1145/3497775.3503679⟩. ⟨hal-03200774v2⟩
  • David Monniaux, Sylvain Boulmé. The Trusted Computing Base of the CompCert Verified Compiler. Programming Languages and Systems (ESOP 2022), Apr 2022, Munich, Germany. pp.204-233, ⟨10.1007/978-3-030-99336-8_8⟩. ⟨hal-03541595⟩
  • David Monniaux, Cyril Six. Simple, Light, Yet Formally Verified, Global Common Subexpression Elimination and Loop-Invariant Code Motion. Languages, Compilers, Tools and Theory of Embedded Systems (LCTES), ACM, Jun 2021, online, Canada. pp.85-96, ⟨10.1145/3461648.3463850⟩. ⟨hal-03212087⟩
  • Julien Braine, Laure Gonnord, David Monniaux. Data Abstraction: A General Framework to Handle Program Verification of Data Structures. SAS 2021 - 28th Static Analysis Symposium, Oct 2021, Chicago, United States. pp.215-235, ⟨10.1007/978-3-030-88806-0_11⟩. ⟨hal-03321868⟩
  • Hang yu, David Monniaux. An Efficient Parametric Linear Programming Solver and Application to Polyhedral Projection. Static Analysis (SAS 2019), Oct 2019, Porto, Portugal. pp.203-224, ⟨10.1007/978-3-030-32304-2_11⟩. ⟨hal-02362102⟩
  • Camille Coti, David Monniaux, Hang yu. Parallel parametric linear programming solving, and application to polyhedral computations. International conference on computational science, Jun 2019, Faro, Portugal. pp.566-572, ⟨10.1007/978-3-030-22750-0_52⟩. ⟨hal-02097321⟩
  • Sylvain Boulmé, Alexandre Maréchal, David Monniaux, Michaël Périn, Hang yu. The Verified Polyhedron Library: an overview. 20th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC), Universitatea de Vest din Timișoara, Sep 2018, Timișoara, Romania. pp.9-17. ⟨hal-02100006⟩
  • Alexey Bakhirkin, David Monniaux. Extending Constraint-Only Representation of Polyhedra with Boolean Constraints. 25th Static Analysis Symposium (SAS 2018), Aug 2018, Freiburg im Breisgau, Germany. pp.127-145, ⟨10.1007/978-3-319-99725-4_10⟩. ⟨hal-01841837v2⟩
  • Alexey Bakhirkin, David Monniaux. Combining Forward and Backward Abstract Interpretation of Horn Clauses. 24th International Static Analysis Symposium (SAS), Francesco Ranzato; Patrick Cousot, Aug 2017, New York City, United States. ⟨hal-01551447v2⟩
  • Claire Maïza, Valentin Touzeau, David Monniaux, Jan Reineke. Ascertaining Uncertainty for Efficient Exact Cache Analysis: Tech report. Extended version of CAV 2017 "Ascertaining Uncertainty for Efficient Exact Cache Analysis" paper. Computer Aided Verification - 29th International Conference, Rupak Majumdar; Viktor Kuncak, Jul 2017, Heidelberg, France. pp.20 - 40, ⟨10.1007/978-3-319-63390-9_2⟩. ⟨hal-01592048v2⟩
  • Alexandre Maréchal, David Monniaux, Michaël Périn. Scalable Minimizing-Operators on Polyhedra via Parametric Linear Programming. Static Analysis Symposium (SAS), Francesco Ranzato, Aug 2017, New York, United States. ⟨hal-01555998⟩
  • David Monniaux, Laure Gonnord. Cell morphing: from array programs to array-free Horn clauses. 23rd Static Analysis Symposium (SAS 2016), Sep 2016, Edimbourg, United Kingdom. ⟨hal-01206882v3⟩
  • Valentin Touzeau, Claire Maïza, David Monniaux. Model Checking of Cache for WCET Analysis Refinement. 10th Junior Researcher Workshop on Real-Time Computing, Oct 2016, Brest, France. ⟨hal-01447930v2⟩
  • Alexandre Maréchal, Alexis Fouilhé, Tim King, David Monniaux, Michaël Périn. Polyhedral Approximation of Multivariate Polynomials using Handelman's Theorem. International Conference on Verification, Model Checking, and Abstract Interpretation 2016, Barbara Jobstmann; Rustan Leino, Jan 2016, St. Petersburg, United States. ⟨hal-01223362⟩
  • Egor George Karpenkov, David Monniaux, Wendler Philipp. Program Analysis with Local Policy Iteration. Verification, Model Checking, and Abstract Interpretation (VMCAI), Jan 2016, Saint Petersburg, Florida, United States. pp.127-146, ⟨10.1007/978-3-662-49122-5_6⟩. ⟨hal-01255314⟩
  • David Monniaux. A Survey of Satisfiability Modulo Theory. Computer Algebra in Scientific Computing, Sep 2016, Bucharest, Romania. ⟨hal-01332051⟩
  • Egor George Karpenkov, David Monniaux. Formula Slicing: Inductive Invariants from Preconditions. 12th International Haifa Verification Conference (HVC), Nov 2016, Haifa, Israel. pp.169-185, ⟨10.1007/978-3-319-49052-6_11⟩. ⟨hal-01446354⟩
  • David Monniaux, Francesco Alberti. A simple abstraction of arrays and maps by program translation. 22nd International Static Analysis Symposium (SAS), Sep 2015, Saint-Malo, France. pp.217-234, ⟨10.1007/978-3-662-48288-9_13⟩. ⟨hal-01162795⟩
  • Francesco Alberti, David Monniaux. Polyhedra to the rescue of array interpolants. ACM/SIGAPP Symposium On Applied Computing, Apr 2015, Salamanca, Spain. ⟨hal-01178600⟩
  • Laure Gonnord, David Monniaux, Gabriel Radanne. Synthesis of ranking functions using extremal counterexamples. Programming Languages, Design and Implementation, Jun 2015, Portland, Oregon, United States. ⟨10.1145/2737924.2737976⟩. ⟨hal-01144622⟩
  • Julien Henry, Mihail Asavoae, David Monniaux, Claire Maïza. How to Compute Worst-Case Execution Time by Optimization Modulo Theory and a Clever Encoding of Program Semantics. ACM SIGPLAN/SIGBED Conference on Languages, Compilers and Tools for Embedded Systems 2014, Jun 2014, Edimbourg, United Kingdom. pp.1-10. ⟨hal-00998138⟩
  • Alexis Fouilhé, David Monniaux, Michaël Périn. Efficient Generation of Correctness Certificates for the Abstract Domain of Polyhedra. 20th static analysis symposium (SAS), Jun 2013, Seattle, Washington, United States. pp.345-365, ⟨10.1007/978-3-642-38856-9_19⟩. ⟨hal-00806990⟩
  • Thomas Braibant, Jacques-Henri Jourdan, David Monniaux. Implementing hash-consed structures in Coq. Interactive Theorem Proving, 4th international conference, Jul 2013, Rennes, France. pp.477-483, ⟨10.1007/978-3-642-39634-2_36⟩. ⟨hal-00816672⟩
  • Julien Henry, David Monniaux, Matthieu Moy. PAGAI: a path sensitive static analyzer. Tools for Automatic Program AnalysiS (TAPAS 2012), Sep 2012, Deauville, France. pp.3. ⟨hal-00718438⟩
  • Anh-Dung Phan, Nikolaj Bjørner, David Monniaux. Anatomy of Alternating Quantifier Satisfiability (Work in progress). 10th International Workshop on Satisfiability Modulo Theories, Jun 2012, Manchester, United Kingdom. pp.6. ⟨hal-00716323⟩
  • Julien Henry, David Monniaux, Matthieu Moy. Succinct Representations for Abstract Interpretation. Static analysis symposium (SAS), Sep 2012, Deauville, France. pp.283-299, ⟨10.1007/978-3-642-33125-1_20⟩. ⟨hal-00709833⟩
  • Thomas Martin Gawlitza, David Monniaux. Improving Strategies via SMT Solving. European symposium on programming (ESOP 2011), Mar 2011, Saarbrücken, Germany. pp.236-255, ⟨10.1007/978-3-642-19718-5_13⟩. ⟨hal-00555795⟩
  • David Monniaux, Laure Gonnord. Using Bounded Model Checking to Focus Fixpoint Iterations. Static analysis symposium (SAS), Sep 2011, Venezia, Italy. pp.369-385, ⟨10.1007/978-3-642-23702-7_27⟩. ⟨hal-00600087⟩
  • David Monniaux, Martin Bodin. Modular Abstractions of Reactive Nodes using Disjunctive Invariants. Asian symposium on programming languages and systems (APLAS), Dec 2011, Kenting, Taiwan. pp.19-33, ⟨10.1007/978-3-642-25318-8_5⟩. ⟨hal-00620682⟩
  • David Monniaux, Pierre Corbineau. On the Generation of Positivstellensatz Witnesses in Degenerate Cases. Interactive Theorem Proving, Aug 2011, Nijmegen, Netherlands. pp.249-264. ⟨hal-00594761⟩
  • David Monniaux. Quantifier elimination by lazy model enumeration. CAV 2010, Jul 2010, Edimburgh, United Kingdom. pp.585-599. ⟨hal-00472831v2⟩
  • David Monniaux. On using floating-point computations to help an exact linear arithmetic decision procedure. Computer-aided verification (CAV 2009), Jun 2009, Grenoble, France. pp.570-583. ⟨hal-00354112v2⟩
  • David Monniaux. Automatic Modular Abstractions for Linear Constraints. POPL 2009, 36th annual ACM SIGPLAN/SIGACT Symposium on Principles of Programming Languages, Jan 2009, Savannah, Georgia, United States. pp.140-151. ⟨hal-00336144⟩
  • David Monniaux. A Quantifier Elimination Algorithm for Linear Real Arithmetic. LPAR ( Logic for Programming, Artificial Intelligence, and Reasoning), Nov 2008, Doha, Qatar. pp.243-257, ⟨10.1007/978-3-540-89439-1_18⟩. ⟨hal-00262312v2⟩
  • David Monniaux. Verification of Device Drivers and Intelligent Controllers: a Case Study. International Conference On Embedded Software (EMSOFT), Sep 2007, Salzburg, Austria. pp.30 - 36, ⟨10.1145/1289927.1289937⟩. ⟨hal-00158869⟩
  • Patrick Cousot, Radhia Cousot, Jerôme Feret, Laurent Mauborgne, Antoine Miné, et al.. Varieties of Static Analyzers: A Comparison with ASTRÉE. First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering (TASE '07), Jun 2007, Shanghai, China. pp.3-20, ⟨10.1109/TASE.2007.55⟩. ⟨hal-00154031⟩
  • David Monniaux. Optimal abstraction on real-valued programs. 14th International Static Analysis Symposium (SAS 2007), 2007, Kongens Lyngby, Denmark. pp.104-120, ⟨10.1007/978-3-540-74061-2_7⟩. ⟨hal-00148608⟩
  • Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, et al.. Combination of Abstractions in the ASTRÉE Static Analyzer. the 11th Annual Asian Computing Science Conference - ASIAN'06, Okada, Mitsu and Satoh, Ichir, Dec 2006, Tokyo, Japan. pp.272-300, ⟨10.1007/978-3-540-77505-8_23⟩. ⟨inria-00528571⟩
  • David Monniaux. Compositional analysis of floating-point linear numerical filters. 2005, pp.199, ⟨10.1007/11513988_21⟩. ⟨hal-00084291⟩
  • David Monniaux. The parallel implementation of the Astrée static analyzer. 2005, pp.86-96, ⟨10.1007/11575467_7⟩. ⟨hal-00128097⟩
  • Patrick Cousot, Radhia Cousot, Jerôme Feret, Laurent Mauborgne, Antoine Miné, et al.. The ASTRÉE analyzer. 2005, pp.21, ⟨10.1007/b107380⟩. ⟨hal-00084293⟩
  • Bruno Blanchet, Patrick Cousot, Radhia Cousot, Jerôme Feret, Laurent Mauborgne, et al.. A Static Analyzer for Large Safety-Critical Software. 2003, pp.196 - 207, ⟨10.1145/781131.781153⟩. ⟨hal-00128135⟩
  • David Monniaux. An Abstract Monte-Carlo Method for the Analysis of Probabilistic Programs. 2001, pp.93 - 101, ⟨10.1145/360204.360211⟩. ⟨hal-00128138⟩

Book sections2 documents

  • David Monniaux. Il faut se défier de la « pensée magique » : 5 questions à David Monniaux. Gilles Rouet. Algorithmes et décisions publiques, CNRS Éditions, 2019, 978-2-271-12466-1. ⟨hal-02043272⟩
  • Bruno Blanchet, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, et al.. Design and Implementation of a Special-Purpose Static Program Analyzer for Safety-Critical Real-Time Embedded Software. Mogensen, T. and Schmidt, D.A. and Sudborough, I.H. The Essence of Computation: Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones, 2566, Springer, pp.85-108, 2002, Lecture Notes in Computer Science, ⟨10.1007/3-540-36377-7_5⟩. ⟨inria-00528442⟩

Directions of work or proceedings1 document

  • Ahmed Bouajjani, David Monniaux. Verification, Model Checking, and Abstract Interpretation. Verification, Model Checking, and Abstract Interpretation (VMCAI), Jan 2017, Paris, France. 10145, Springer, 2017, 978-3-319-52233-3. ⟨10.1007/978-3-319-52234-0⟩. ⟨hal-01446363⟩

Preprints, Working Papers, ...5 documents

  • David Monniaux. NP #P = ∃PP and other remarks about maximized counting. 2022. ⟨hal-03586193⟩
  • David Monniaux. On using sums-of-squares for exact computations without strict feasibility. 2010. ⟨hal-00487279⟩
  • David Monniaux. On computing invariants for predicate abstraction by SAT-solving. 2009. ⟨hal-00357118⟩
  • David Monniaux. Fatal Degeneracy in the Semidefinite Programming Approach to the Decision of Polynomial Inequalities. 2009. ⟨hal-00357358⟩
  • David Monniaux. Applying the Z-transform for the static analysis of floating-point numerical filters. 2005. ⟨hal-00151251⟩

Reports2 documents

  • Julien Braine, Laure Gonnord, David Monniaux. Data Abstraction: A General Framework to Handle Program Verification of Data Structures. [Research Report] RR-9408, Inria Grenoble Rhône-Alpes; VERIMAG UMR 5104, Université Grenoble Alpes, France; LIP - Laboratoire de l’Informatique du Parallélisme; Université Lyon 1 - Claude Bernard; ENS Lyon. 2021, pp.1-29. ⟨hal-03214475v2⟩
  • Julien Braine, Laure Gonnord, David Monniaux. Verifying Programs with Arrays and Lists. [Internship report] ENS Lyon. 2016. ⟨hal-01337140⟩

Theses1 document

  • David Monniaux. Analysis of probabilistic programs by abstract interpretation. Software Engineering [cs.SE]. Université Paris Dauphine - Paris IX, 2001. English. ⟨tel-00084287⟩

Habilitation à diriger des recherches1 document

  • David Monniaux. Analyse statique : de la théorie à la pratique ; analyse statique de code embarqué de grande taille, génération de domaines abstraits. Génie logiciel [cs.SE]. Université Joseph-Fourier - Grenoble I, 2009. ⟨tel-00397108⟩