Number of documents

59

David Monniaux


Journal articles9 documents

Conference papers35 documents

  • 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⟩
  • 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⟩
  • 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 Maiza, Valentin Touzeau, Claire Ma¨ıza, 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⟩
  • 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⟩
  • Egor 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⟩
  • 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⟩
  • David Monniaux. A Survey of Satisfiability Modulo Theory. Computer Algebra in Scientific Computing, Sep 2016, Bucharest, Romania. ⟨hal-01332051⟩
  • Egor 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, 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⟩
  • 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⟩
  • 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⟩
  • 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⟩
  • 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⟩
  • 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⟩
  • 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, 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, 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. Quantifier elimination by lazy model enumeration. CAV 2010, Jul 2010, Edimburgh, United Kingdom. pp.585-599. ⟨hal-00472831v2⟩
  • 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. 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. 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⟩
  • 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. 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⟩
  • 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. The parallel implementation of the Astrée static analyzer. 2005, pp.86-96, ⟨10.1007/11575467_7⟩. ⟨hal-00128097⟩
  • David Monniaux. Compositional analysis of floating-point linear numerical filters. 2005, pp.199, ⟨10.1007/11513988_21⟩. ⟨hal-00084291⟩
  • 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. ⟨http://www.cnrseditions.fr/⟩. ⟨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, ...9 documents

  • Sylvain Boulmé, Alexandre Maréchal, David Monniaux, Michaël Périn, Hang Yu. The Verified Polyhedron Library: an overview. 2019. ⟨hal-02100006⟩
  • Camille Coti, David Monniaux, Hang Yu. Parallel parametric linear programming solving, and application to polyhedral computations. 2019. ⟨hal-02097321⟩
  • David Monniaux, Valentin Touzeau. On the complexity of cache analysis for different replacement policies. 2018. ⟨hal-01910216⟩
  • David Monniaux, Julien Le Guen. Stratified Static Analysis Based on Variable Dependencies. 2011. ⟨hal-00622137⟩
  • Thomas Gawlitza, David Monniaux. Improving Strategies via SMT Solving. 2011. ⟨hal-00555795⟩
  • 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⟩

Reports1 document

  • Julien Braine, Laure Gonnord, David Monniaux. Verifying Programs with Arrays and Lists. [Intership 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⟩