Difference between revisions of "Grenoble meeting 27 February 2015"
| Line 1: | Line 1: | ||
9h30 '''Coffee+croissants''' | 9h30 '''Coffee+croissants''' | ||
| − | 10h00 '''Marek Trtik''' (Verimag) | + | 10h00 '''Marek Trtik''' (Verimag) ''Formula-based Communication Between Program Analyses'' |
| − | + | ||
| − | ''Formula-based Communication Between Program Analyses'' | + | |
A promising approach to checking of program properties is to combine some existing analyses into a better one ideally comprising the union of strengths and the intersection of weaknesses of individual techniques. Unfortunately, the approach is difficult in general as different analyses use different formalisms and build different models of an analysed program. We propose a new approach where individual analyses exchange their knowledge about memory content during their simultaneous execution via a formula-based communication language in order to mutually improve their own precision. The language is analysis-independent and so we can combine arbitrarily many analyses without writing a line of code relating any pair of contributing analyses. Moreover, we show that all static analyses we considered (two abstract interpretations (intervals and polyhedrons) and the classic King's symbolic execution) adopted the concept of the communication very naturally. Finally, although combining analyses by providing a dedicated code may often lead to better results (because of the generality of our communication concept), we show in our experimental evaluation on SV-COMP benchmark suite that our approach indeed provides interesting results in term of improved precision of computed invariants. | A promising approach to checking of program properties is to combine some existing analyses into a better one ideally comprising the union of strengths and the intersection of weaknesses of individual techniques. Unfortunately, the approach is difficult in general as different analyses use different formalisms and build different models of an analysed program. We propose a new approach where individual analyses exchange their knowledge about memory content during their simultaneous execution via a formula-based communication language in order to mutually improve their own precision. The language is analysis-independent and so we can combine arbitrarily many analyses without writing a line of code relating any pair of contributing analyses. Moreover, we show that all static analyses we considered (two abstract interpretations (intervals and polyhedrons) and the classic King's symbolic execution) adopted the concept of the communication very naturally. Finally, although combining analyses by providing a dedicated code may often lead to better results (because of the generality of our communication concept), we show in our experimental evaluation on SV-COMP benchmark suite that our approach indeed provides interesting results in term of improved precision of computed invariants. | ||
| − | 10h30 '''Boris Yakobovski''' (CEA) | + | 10h30 '''Boris Yakobovski''' (CEA) ''Improving Static Analyses of C Programs with Conditional Predicates'' |
| − | + | ||
| − | ''Improving Static Analyses of C Programs with Conditional Predicates'' | + | |
Designing sound static analyses is a continuing trade-off between precision and complexity. Notably, dataflow analyses often perform overly wide approximations when two control-flow paths meet, by merging states from each path. This paper presents a generic abstract interpretation based framework to enhance the precision of such analyses on join points. It relies on predicated domains, that preserve and reuse information valid only inside some branches of the code. Our predicates are derived from conditional statements, and postpone the loss of information. The work has been integrated into Frama-C, a C source code analysis platform. Experiments on real code show that our approach scales, and improves significantly the precision of the existing analyses of Frama-C. | Designing sound static analyses is a continuing trade-off between precision and complexity. Notably, dataflow analyses often perform overly wide approximations when two control-flow paths meet, by merging states from each path. This paper presents a generic abstract interpretation based framework to enhance the precision of such analyses on join points. It relies on predicated domains, that preserve and reuse information valid only inside some branches of the code. Our predicates are derived from conditional statements, and postpone the loss of information. The work has been integrated into Frama-C, a C source code analysis platform. Experiments on real code show that our approach scales, and improves significantly the precision of the existing analyses of Frama-C. | ||
| − | 11h00 '''Mihaela Sighireanu''' (LIAFA) | + | 11h00 '''Mihaela Sighireanu''' (LIAFA) ''Automating Program Proofs Based on Separation Logic with Inductive Definitions'' |
| − | + | ||
| − | ''Automating Program Proofs Based on Separation Logic with Inductive Definitions'' | + | |
We propose a novel approach for exploiting the inductive definitions in automating program proofs based on inductive invariants. We focus on iterative programs, although our techniques apply to recursive programs as well, and specifications that describe not only the shape of the data structures, but also their content or their size.Empirically, we find that our approach is powerful enough to deal with sophisticated benchmarks, e.g., iterative procedures for searching, inserting, or delet- ing elements in binary search tress, red-black trees, and AVL trees, in a very efficient way. Joint work with C. Enea and Z. Wu. | We propose a novel approach for exploiting the inductive definitions in automating program proofs based on inductive invariants. We focus on iterative programs, although our techniques apply to recursive programs as well, and specifications that describe not only the shape of the data structures, but also their content or their size.Empirically, we find that our approach is powerful enough to deal with sophisticated benchmarks, e.g., iterative procedures for searching, inserting, or delet- ing elements in binary search tress, red-black trees, and AVL trees, in a very efficient way. Joint work with C. Enea and Z. Wu. | ||
| − | 11h30 '''Radu Iosif''' (VERIMAG) | + | 11h30 '''Radu Iosif''' (VERIMAG) ''Abstraction Refinement for Trace Inclusion of Infinite State Systems'' |
| − | + | ||
| − | ''Abstraction Refinement for Trace Inclusion of Infinite State Systems'' | + | |
A data automaton is a finite automaton equipped with variables (counters or registers) ranging over infinite data domains. A trace of a data automaton is an alternating sequence of alphabet symbols and values taken by the counters during an execution of the automaton. The problem addressed in this paper is the inclusion between the sets of traces (data languages) recognized by such automata. Since the problem is undecidable, we give a semi-algorithm based on abstraction refinement, which is proved to be sound and complete, but whose termination is not guaranteed. We have implemented our technique in a prototype tool and show promising results on several non-trivial examples. | A data automaton is a finite automaton equipped with variables (counters or registers) ranging over infinite data domains. A trace of a data automaton is an alternating sequence of alphabet symbols and values taken by the counters during an execution of the automaton. The problem addressed in this paper is the inclusion between the sets of traces (data languages) recognized by such automata. Since the problem is undecidable, we give a semi-algorithm based on abstraction refinement, which is proved to be sound and complete, but whose termination is not guaranteed. We have implemented our technique in a prototype tool and show promising results on several non-trivial examples. | ||
| Line 27: | Line 19: | ||
12h00 '''Lunch''' (on site) | 12h00 '''Lunch''' (on site) | ||
| − | 13h30 '''Cristina Serban''' (VERIMAG) | + | 13h30 '''Cristina Serban''' (VERIMAG) ''A Formalization of Separation Logic in SMT_LIB V2.5: Syntax, Types and Semantics'' |
| − | + | ||
| − | ''A Formalization of Separation Logic in SMT_LIB V2.5: Syntax, Types and Semantics'' | + | |
14h00 '''Business Meeting''' | 14h00 '''Business Meeting''' | ||
17h00 '''Coffee break''' | 17h00 '''Coffee break''' | ||
Revision as of 20:11, 18 February 2015
9h30 Coffee+croissants
10h00 Marek Trtik (Verimag) Formula-based Communication Between Program Analyses
A promising approach to checking of program properties is to combine some existing analyses into a better one ideally comprising the union of strengths and the intersection of weaknesses of individual techniques. Unfortunately, the approach is difficult in general as different analyses use different formalisms and build different models of an analysed program. We propose a new approach where individual analyses exchange their knowledge about memory content during their simultaneous execution via a formula-based communication language in order to mutually improve their own precision. The language is analysis-independent and so we can combine arbitrarily many analyses without writing a line of code relating any pair of contributing analyses. Moreover, we show that all static analyses we considered (two abstract interpretations (intervals and polyhedrons) and the classic King's symbolic execution) adopted the concept of the communication very naturally. Finally, although combining analyses by providing a dedicated code may often lead to better results (because of the generality of our communication concept), we show in our experimental evaluation on SV-COMP benchmark suite that our approach indeed provides interesting results in term of improved precision of computed invariants.
10h30 Boris Yakobovski (CEA) Improving Static Analyses of C Programs with Conditional Predicates
Designing sound static analyses is a continuing trade-off between precision and complexity. Notably, dataflow analyses often perform overly wide approximations when two control-flow paths meet, by merging states from each path. This paper presents a generic abstract interpretation based framework to enhance the precision of such analyses on join points. It relies on predicated domains, that preserve and reuse information valid only inside some branches of the code. Our predicates are derived from conditional statements, and postpone the loss of information. The work has been integrated into Frama-C, a C source code analysis platform. Experiments on real code show that our approach scales, and improves significantly the precision of the existing analyses of Frama-C.
11h00 Mihaela Sighireanu (LIAFA) Automating Program Proofs Based on Separation Logic with Inductive Definitions
We propose a novel approach for exploiting the inductive definitions in automating program proofs based on inductive invariants. We focus on iterative programs, although our techniques apply to recursive programs as well, and specifications that describe not only the shape of the data structures, but also their content or their size.Empirically, we find that our approach is powerful enough to deal with sophisticated benchmarks, e.g., iterative procedures for searching, inserting, or delet- ing elements in binary search tress, red-black trees, and AVL trees, in a very efficient way. Joint work with C. Enea and Z. Wu.
11h30 Radu Iosif (VERIMAG) Abstraction Refinement for Trace Inclusion of Infinite State Systems
A data automaton is a finite automaton equipped with variables (counters or registers) ranging over infinite data domains. A trace of a data automaton is an alternating sequence of alphabet symbols and values taken by the counters during an execution of the automaton. The problem addressed in this paper is the inclusion between the sets of traces (data languages) recognized by such automata. Since the problem is undecidable, we give a semi-algorithm based on abstraction refinement, which is proved to be sound and complete, but whose termination is not guaranteed. We have implemented our technique in a prototype tool and show promising results on several non-trivial examples.
12h00 Lunch (on site)
13h30 Cristina Serban (VERIMAG) A Formalization of Separation Logic in SMT_LIB V2.5: Syntax, Types and Semantics
14h00 Business Meeting
17h00 Coffee break
