David Monniaux

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. 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⟩

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, 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⟩

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. 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⟩

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⟩

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⟩

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⟩

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⟩

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⟩

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⟩

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⟩

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⟩

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. A Survey of Satisfiability Modulo Theory. Computer Algebra in Scientific Computing, Sep 2016, Bucharest, Romania. ⟨hal-01332051⟩

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⟩

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⟩

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⟩

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⟩

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. 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. 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⟩

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⟩

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, 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⟩

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⟩

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⟩

Thomas Gawlitza, David Monniaux. Improving Strategies via SMT Solving. 2011. ⟨hal-00555795⟩

David Monniaux, Julien Le Guen. Stratified Static Analysis Based on Variable Dependencies. 2011. ⟨hal-00622137⟩

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⟩

Julien Braine, Laure Gonnord, David Monniaux. Verifying Programs with Arrays and Lists. [Intership report] ENS Lyon. 2016. ⟨hal-01337140⟩

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

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⟩