Nombre de documents

53

David Monniaux


Article dans une revue7 documents

Communication dans un congrès34 documents

  • Alexandre Maréchal, David Monniaux, Michaël Périn. Scalable Minimizing-Operators on Polyhedra via Parametric Linear Programming. Springer-Verlag. Static Analysis Symposium (SAS), Aug 2017, New York, United States. 10422, 2017, Lecture Notes in Computer Science. 〈hal-01555998〉
  • Alexey Bakhirkin, David Monniaux. Combining Forward and Backward Abstract Interpretation of Horn Clauses. Francesco Ranzato. 24th International Static Analysis Symposium (SAS), Aug 2017, New York City, United States. Springer, Static Analysis. 〈http://staticanalysis.org/sas2017/sas2017.html〉. 〈hal-01551447v2〉
  • Valentin Touzeau, Claire Maiza, 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. Rupak Majumdar; Viktor Kuncak. Computer Aided Verification - 29th International Conference, Jul 2017, Heidelberg, France. Springer, 10427 (2), pp.20 - 40, 2017, Lecture notes in computer science. 〈http://cavconference.org/2017/〉. 〈10.1145/216585.216588〉. 〈hal-01592048〉
  • 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, Jan 2016, St. Petersburg, United States. International Conference on Verification, Model Checking, and Abstract Interpretation 2016, 2015. 〈hal-01223362〉
  • Valentin Touzeau, Claire Maïza, David Monniaux. Model Checking of Cache for WCET Analysis Refinement. Antoine Bertout; Martina Maggio. 10th Junior Researcher Workshop on Real-Time Computing, Oct 2016, Brest, France. 〈http://jrwrtc2016.gforge.inria.fr/〉. 〈hal-01447930v2〉
  • David Monniaux, Laure Gonnord. Cell morphing: from array programs to array-free Horn clauses. Xavier Rival. 23rd Static Analysis Symposium (SAS 2016), Sep 2016, Edimbourg, United Kingdom. Static Analysis Symposium, Static Analysis Symposium. 〈http://staticanalysis.org/sas2016〉. 〈hal-01206882v3〉
  • Egor Karpenkov, David Monniaux, Wendler Philipp. Program Analysis with Local Policy Iteration. Barbara Jobstmann; K. Rustan M. Leino. Verification, Model Checking, and Abstract Interpretation (VMCAI), Jan 2016, Saint Petersburg, Florida, United States. Springer, 9583, pp.127-146, 2015, 〈http://conf.researchr.org/home/VMCAI-2016〉. 〈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. 2016. 〈hal-01332051〉
  • Egor Karpenkov, David Monniaux. Formula Slicing: Inductive Invariants from Preconditions. Roderick Bloem; Eli Arbel. 12th International Haifa Verification Conference (HVC), Nov 2016, Haifa, Israel. Springer, Lectures Notes in Computer Science, 10028, pp.169-185, 〈https://www.research.ibm.com/haifa/conferences/hvc2016/〉. 〈10.1007/978-3-319-49052-6_11〉. 〈hal-01446354〉
  • David Monniaux, Francesco Alberti. A simple abstraction of arrays and maps by program translation. Sandrine Blazy; Thomas Jensen. 22nd International Static Analysis Symposium (SAS), Sep 2015, Saint-Malo, France. Springer, Lecture Notes in Computer Science, 9291, pp.217-234, Static Analysis. 〈http://sas2015.inria.fr/〉. 〈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. Association for computing machinery, 2015. 〈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. Association for Computing Machinery, pp.1-10, 2014. 〈hal-00998138〉
  • Thomas Braibant, Jacques-Henri Jourdan, David Monniaux. Implementing hash-consed structures in Coq. Sandrine Blazy and Christine Paulin-Mohring and David Pichardie. Interactive Theorem Proving, 4th international conference, Jul 2013, Rennes, France. Springer, 7998, pp.477-483, 2013, Lecture notes in computer science. 〈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. Francesco Logozzo, Manuel Fähndrich. 20th static analysis symposium (SAS), Jun 2013, Seattle, Washington, United States. Springer, 7935, pp.345-365, 2013, 〈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, 2012. 〈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, 2012. 〈hal-00718438〉
  • Julien Henry, David Monniaux, Matthieu Moy. Succinct Representations for Abstract Interpretation. Static analysis symposium (SAS), Sep 2012, Deauville, France. Springer, pp.283-299, 2012, Lecture notes in Computer Science. 〈10.1007/978-3-642-33125-1_20〉. 〈hal-00709833〉
  • David Monniaux, Martin Bodin. Modular Abstractions of Reactive Nodes using Disjunctive Invariants. Hongseok Yang. Asian symposium on programming languages and systems (APLAS), Dec 2011, Kenting, Taiwan. Springer, 7078, pp.19-33, 2011, LNCS. 〈10.1007/978-3-642-25318-8_5〉. 〈hal-00620682〉
  • David Monniaux, Laure Gonnord. Using Bounded Model Checking to Focus Fixpoint Iterations. Eran Yahav. Static analysis symposium (SAS), Sep 2011, Venezia, Italy. Springer, 6887, pp.369-385, 2011, Lecture notes in Computer Science. 〈10.1007/978-3-642-23702-7_27〉. 〈hal-00600087〉
  • David Monniaux, Pierre Corbineau. On the Generation of Positivstellensatz Witnesses in Degenerate Cases. Van Eekelen, M.; Geuvers, H.; Schmaltz, J.; Wiedijk, F. Interactive Theorem Proving, Aug 2011, Nijmegen, Netherlands. Springer, 6898, pp.249-264, 2011, Lecture notes in Computer Science. 〈hal-00594761〉
  • David Monniaux. Quantifier elimination by lazy model enumeration. Byron Cook, Paul Jackson, Tayssir Touili. CAV 2010, Jul 2010, Edimburgh, United Kingdom. Springer-Verlag, 6174, pp.585-599, 2010, Lecture notes in computer science. 〈hal-00472831v2〉
  • David Monniaux. Automatic Modular Abstractions for Linear Constraints. Benjamin C. Pierce. POPL 2009, 36th annual ACM SIGPLAN/SIGACT Symposium on Principles of Programming Languages, Jan 2009, Savannah, Georgia, United States. ACM, pp.140-151, 2009. 〈hal-00336144〉
  • David Monniaux. On using floating-point computations to help an exact linear arithmetic decision procedure. Ahmed Bouajjani, Oded Maler. Computer-aided verification (CAV 2009), Jun 2009, Grenoble, France. Springer-Verlag, 5643, pp.570-583, 2009, Lecture notes in computer science. 〈hal-00354112v2〉
  • David Monniaux. A Quantifier Elimination Algorithm for Linear Real Arithmetic. Iliano Cervesato, Helmut Veith, Andrei Voronkov. LPAR ( Logic for Programming, Artificial Intelligence, and Reasoning), Nov 2008, Doha, Qatar. Springer, 5330, pp.243-257, 2008, Lecture notes in computer science. 〈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. He Jifeng, Jeff Sanders. First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering (TASE '07), Jun 2007, Shanghai, China. First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering, 2007. TASE '07, pp.3-20, 2007, 〈10.1109/TASE.2007.55〉. 〈hal-00154031〉
  • David Monniaux. Verification of Device Drivers and Intelligent Controllers: a Case Study. Christoph M. Kirsch, Reinhard Wilhelm. International Conference On Embedded Software (EMSOFT), Sep 2007, Salzburg, Austria. ACM, pp.30 - 36, 2007, 〈10.1145/1289927.1289937〉. 〈hal-00158869〉
  • David Monniaux. Optimal abstraction on real-valued programs. Gilberto Filé, Hanne Riis Nielson. 14th International Static Analysis Symposium (SAS 2007), 2007, Kongens Lyngby, Denmark. Springer, pp.104-120, 2007, LNCS 4634. 〈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. Okada, Mitsu and Satoh, Ichir. the 11th Annual Asian Computing Science Conference - ASIAN'06, Dec 2006, Tokyo, Japan. Springer, 4435, pp.272-300, 2006, Lecture Notes in Computer Science. 〈10.1007/978-3-540-77505-8_23〉. 〈inria-00528571〉
  • Patrick Cousot, Radhia Cousot, Jerôme Feret, Laurent Mauborgne, Antoine Miné, et al.. The ASTRÉE analyzer. Mooly Sagiv. 2005, Springer, pp.21, 2005, LNCS #3444. 〈10.1007/b107380〉. 〈hal-00084293〉
  • David Monniaux. Compositional analysis of floating-point linear numerical filters. Kousha Etessami, Sriram K. Rajamani. 2005, Springer, pp.199, 2005, Lecture notes in computer science #3576. 〈10.1007/11513988_21〉. 〈hal-00084291〉
  • David Monniaux. The parallel implementation of the Astrée static analyzer. Kwangkeun Yi. 2005, Springer, pp.86-96, 2005, LNCS 3780. 〈10.1007/11575467_7〉. 〈hal-00128097〉
  • Bruno Blanchet, Patrick Cousot, Radhia Cousot, Jerôme Feret, Laurent Mauborgne, et al.. A Static Analyzer for Large Safety-Critical Software. Rajiv Gupta. 2003, Association for Computer Machinery (ACM), pp.196 - 207, 2003, 〈10.1145/781131.781153〉. 〈hal-00128135〉
  • David Monniaux. An Abstract Monte-Carlo Method for the Analysis of Probabilistic Programs. Chris Hankin, Dave Schmidt. 2001, Association for Computer Machinery (ACM), pp.93 - 101, 2001, 〈10.1145/360204.360211〉. 〈hal-00128138〉

Chapitre d'ouvrage1 document

  • 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〉

Direction d'ouvrage, Proceedings, Dossier1 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〉

Pré-publication, Document de travail7 documents

  • David Monniaux. On the decidability of the existence of polyhedral invariants in transition systems. 2017. 〈hal-01587125〉
  • 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. Fatal Degeneracy in the Semidefinite Programming Approach to the Decision of Polynomial Inequalities. 2009. 〈hal-00357358〉
  • David Monniaux. On computing invariants for predicate abstraction by SAT-solving. 2009. 〈hal-00357118〉
  • David Monniaux. Applying the Z-transform for the static analysis of floating-point numerical filters. 2005. 〈hal-00151251〉

Rapport1 document

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

Thèse1 document

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

HDR1 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〉