-- Papiers de recherche CR10 / 2016

Affectation :
9) Memory Models -> Raphael Monat
18) Horn -> Valentin Honoré
21) Software MC -> Deak Norbert
8) Comcert -> Clément Sartori.
2) Policy Iteration -> Laureline
15) Tiny OS -> Maverick Chardey
5) IC3 predicate Xavier Montillet
4) IC3 Hardware MC -> V. Lutfalla
13) Parallel cost analysis -> Remy Grunblatt
7) Code optimisation -> Arthur Blot
17) Interpolants -> Panagiotas Ioannis  

-----------------------------------------------------------------------
1)Acceleration (**)
Peter Schrammel and Bertrand Jeannet and Sriram Sankaranarayanan
Abstract Acceleration of General Linear Loops, POPL 2014
http://arxiv.org/abs/1311.0768


2)Policy Iteration (**) 
Thomas Martin Gawlitza, David Monniaux:
Invariant Generation through Strategy Iteration in Succinctly Represented Control Flow Graphs. Logical Methods in Computer Science 8(3) (2012)
http://arxiv.org/pdf/1209.0643v2.pdf


3) Arrays (2 papers) (*)
Aaron R. Bradley, Zohar Manna, Henny B. Sipma, What's Decidable About
Arrays?,  (VMCAI 2006)
http://theory.stanford.edu/~arbrad/papers/arrays.pdf
+ 
R. Iosif, P. Habermehl, and T. Vojnar. What else is de-
cidable about arrays?  FOSSACS 2008 
http://www.liafa.univ-paris-diderot.fr/~haberm/Publications/hiv-arrays-tr-07.pdf


4) SMT- Model Checking (*)
Alberto Griggio and Marco Roveri
Comparing Different Variants of the ic3 Algorithm for Hardware Model Checking
https://people.eecs.berkeley.edu/~alanmi/publications/other/tcad15_pdr.pdf


5) SMT - Predicate abstraction (**)
Alessandro Cimatti, Alberto Griggio, Sergio Mover, Stefano Tonetta:
IC3 Modulo Theories via Implicit Predicate Abstraction
https://arxiv.org/abs/1310.6847

6) Optimisation modulo Theory (**)
Roberto Sebastiani, Patrick Trentin
Pushing the envelope of Optimization Modulo Theories with Linear-Arithmetic Cost Functions
https://arxiv.org/abs/1410.5568


7) Code optimisation (**)
David Menendez, Santosh Nagarakatte and Aarti Gupta. Alive-FP:
Automated Verification of Floating Point Based Peephole Optimizations
in LLVM, SAS 2016
version rapport de recherche ici:
https://www.cs.rutgers.edu/research/technical_reports/report.php?series_id=1&report_id=723


8) Formal verification in Compcert (*)
Sandrine Blazy, André Maroneze, and David Pichardie. Formal
verification of loop bound estimation for WCET analysis. VSTTE 13:
https://www.irisa.fr/celtique/pichardie/papers/vstte13.pdf

9)Memory Models
Thibault Suzanne and Antoine Miné. From array abstract domains to a
parametric abstraction of concurrent programs under store-buffer-based
relaxed memory models SAS16
http://www.di.ens.fr/~suzanne/papers/from_array_domains.pdf


10) Polyhedral algorithmic
Alexis Fouilhé, David Monniaux, Michaël Périn:
Efficient Generation of Correctness Certificates for the Abstract Domain of Polyhedra. SAS 2013: 345-365
https://arxiv.org/pdf/1304.0864v1.pdf

11) Sparse data flow analyses (*)
Parameterized Construction of Program Representations for Sparse
Dataflow Analyses André Tavares (UFMG), Benoit Boissinot (LIP),
Fernando Pereira (LLP), Fabrice Rastello (INRIA)
https://arxiv.org/abs/1403.5952

12) Octagons and sparsity (*) (2 papers)
The Octagon Abstract Domain
https://www-apr.lip6.fr/~mine/publi/article-mine-HOSC06.pdf
+
Jacques-Henri Jourdan. Sparsity preserving algorithms for octagons
NSAD 2016 
https://jhjourdan.mketjh.fr/pdf/jourdan2016sparsity.pdf

13) Termination, cost (**)
Parallel Cost Analysis of Distributed Systems
Elvira Albert, Jesus Correas, Einar Broch Johnsen, Guillermo
Roman-diez, SAS15
http://einarj.at.ifi.uio.no/Papers/albert15sas.pdf

14)  A bit of biology (**)
Context-sensitive flow analyses: a hierarchy of model reductions
Ferdinanda Camporesi Jérôme Feret ,  Jonathan Hayman
https://www.cl.cam.ac.uk/~jmh93/papers/cmsb2013.pdf

15) Concurrent programs (*)
Static analysis by abstract interpretation of functional properties of
device drivers in TinyOS
Abdelraouf Ouadjaout  Antoine Miné, Noureddine Lasla, Nadjib Badache
http://hal.upmc.fr/hal-01350646/document

16) Interpolants (**)
Hossein Hojjat, Radu Iosif, Filip Konecný, Viktor Kuncak, Philipp Rümmer:
Accelerating Interpolants. ATVA 2012: 187-202
https://www.cs.cornell.edu/~hojjat/papers/HojjatETAL12AcceleratingInterpolants.pdf

17) Interpolants and Horn Clauses (**)
Philipp Rümmer, Hossein Hojjat and Viktor Kuncak2
The Relationship between Craig Interpolation and
Recursion-Free Horn Clauses
https://arxiv.org/pdf/1302.4187v1.pdf

18) Horn Clauses (**)
Nikolaj Bjørner, Arie Gurfinkel, Kenneth L. McMillan, Andrey Rybalchenko:
Horn Clause Solvers for Program Verification.
http://www.springer.com/cda/content/document/cda_downloaddocument/9783319235332-c2.pdf?SGWID=0-0-45-1524592-p177657740

20) Arrays (*) --- NE PAS PRENDRE
David Monniaux, Laure Gonnord:
Cell Morphing: From Array Programs to Array-Free Horn Clauses, SAS 16
https://hal.archives-ouvertes.fr/hal-01206882v2/document

21) Software model checking (*)
Matthias Heizmann, Jochen Hoenicke, and Andreas Podelski
Software Model Checking for People who Love Automata
https://swt.informatik.uni-freiburg.de/staff/heizmann/2013cav-heizmann-hoenicke-podelski-software-model-checking-for-people-who-love-automata.pdf