December 2013 - PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(master): Several corrections.
by Roberto Bagnara 30 Dec '13

30 Dec '13

Module: ppl/ppl Branch: master Commit: fdae6f8ee33043bd31efd02fc5246777043a36cc URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=fdae6f8ee330… Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com> Date: Mon Dec 30 09:35:32 2013 +0100 Several corrections. --- doc/ppl_citations.bib | 17 ++++++++--------- 1 files changed, 8 insertions(+), 9 deletions(-) diff --git a/doc/ppl_citations.bib b/doc/ppl_citations.bib index 8d0974e..8ede7c8 100644 --- a/doc/ppl_citations.bib +++ b/doc/ppl_citations.bib @@ -3733,15 +3733,15 @@ Summarizing: to no loss in precision." } -@Inproceedings{MardzielMMS11, - Title = "Dynamic Enforcement of Knowledge-based Security Policies", +@Inproceedings{MardzielMHS11, Author = "P. Mardziel and S. Magill and M. Hicks and M. Srivatsa", + Title = "Dynamic Enforcement of Knowledge-based Security Policies", Year = 2011, Booktitle = "Proceedings of the 24th IEEE Computer Security - Foundations Symposium ({CSF})", + Foundations Symposium (CSF 2011)", Publisher = "IEEE Xplore Digital Library", - Address = "New Orleans, Louisiana, USA", - Editor = "M. Backes and S.Zdancewic", + Address = "Cernay-la-Ville, France", + Editor = "M. Backes and S. Zdancewic", Pages = "114--128", ISBN = "978-0-7695-4365-9", Abstract = "This paper explores the idea of knowledge-based security @@ -4407,11 +4407,10 @@ Summarizing: } @Inproceedings{RastogiMMH13, Author = "A. Rastogi and P. Mardziel and M. Hammer and M. Hicks", - Title = "Knowledge Inference for Optimizing Secure Multi-party Computation", + Title = "Knowledge Inference for Optimizing Secure Multi-Party Computation", Year = 2013, - Booktitle = "{PLAS} '13: - Proceedings of the Eighth ACM SIGPLAN Workshop on - Programming Languages and Analysis for Security", + Booktitle = "Proceedings of the 2013 ACM SIGPLAN Workshop on + Programming Languages and Analysis for Security (PLAS'13)", Editor = "P. Naldurg", ISBN = "978-1-4503-2144-0", Address = "Seattle, Washington, USA",

1 0

[GIT] ppl/ppl(master): Capitalization fixes.
by Roberto Bagnara 30 Dec '13

30 Dec '13

Module: ppl/ppl Branch: master Commit: 7b0e718dfc86e8b3a4e9e467923efb4dcbb7b62c URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=7b0e718dfc86… Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com> Date: Mon Dec 30 08:47:22 2013 +0100 Capitalization fixes. --- doc/ppl_citations.bib | 4 ++-- 1 files changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/ppl_citations.bib b/doc/ppl_citations.bib index 08774df..8d0974e 100644 --- a/doc/ppl_citations.bib +++ b/doc/ppl_citations.bib @@ -3586,7 +3586,7 @@ Summarizing: @Article{LimeMR13, Author = "D. Lime and C. Martinez and O. H. Roux", - Title = "Shrinking of Time Petri nets", + Title = "Shrinking of Time {Petri} Nets", Journal = "Discrete Event Dynamic Systems", Publisher = "Springer-Verlag, Berlin", Volume = 23, @@ -5040,7 +5040,7 @@ Summarizing: @Article{TraonouezLR09, Author = "L.-M. Traonouez and D. Lime and O. H. Roux", - Title = "Parametric Model-Checking of Stopwatch Petri Nets", + Title = "Parametric Model-Checking of Stopwatch {Petri} Nets", Journal = "Journal of Universal Computer Science", Year = 2009, Volume = 15,

1 0

[GIT] ppl/ppl(master): Reference added.
by Patricia Hill 29 Dec '13

29 Dec '13

Module: ppl/ppl Branch: master Commit: cd637456d40bd723746f31594b553e0fa6a66aa5 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=cd637456d40b… Author: Patricia Hill <patricia.hill(a)bugseng.com> Date: Sun Dec 29 21:52:42 2013 +0000 Reference added. --- doc/ppl_citations.bib | 36 ++++++++++++++++++++++++++++++++++++ 1 files changed, 36 insertions(+), 0 deletions(-) diff --git a/doc/ppl_citations.bib b/doc/ppl_citations.bib index e78fcf9..08774df 100644 --- a/doc/ppl_citations.bib +++ b/doc/ppl_citations.bib @@ -3733,6 +3733,42 @@ Summarizing: to no loss in precision." } +@Inproceedings{MardzielMMS11, + Title = "Dynamic Enforcement of Knowledge-based Security Policies", + Author = "P. Mardziel and S. Magill and M. Hicks and M. Srivatsa", + Year = 2011, + Booktitle = "Proceedings of the 24th IEEE Computer Security + Foundations Symposium ({CSF})", + Publisher = "IEEE Xplore Digital Library", + Address = "New Orleans, Louisiana, USA", + Editor = "M. Backes and S.Zdancewic", + Pages = "114--128", + ISBN = "978-0-7695-4365-9", + Abstract = "This paper explores the idea of knowledge-based security + policies, which are used to decide whether to answer + queries over secret data based on an estimation of the + querier's (possibly increased) knowledge given the + results. Limiting knowledge is the goal of existing + information release policies that employ mechanisms such + as noising, anonymization, and + redaction. Knowledge-based policies are more general: + they increase flexibility by not fixing the means to + restrict information flow. We enforce a knowledge-based + policy by explicitly tracking a model of a querier's + belief about secret data, represented as a probability + distribution, and denying any query that could increase + knowledge above a given threshold. We implement query + analysis and belief tracking via abstract interpretation + using a novel probabilistic polyhedral domain, whose + design permits trading off precision with performance + while ensuring estimates of a querier's knowledge are + sound. Experiments with our implementation show that + several useful queries can be handled efficiently, and + performance scales far better than would more standard + implementations of probabilistic computation based on + sampling." +} + @Inproceedings{ManevichSRF04, Author = "R. Manevich and M. Sagiv and G. Ramalingam and J. Field", Title = "Partially Disjunctive Heap Abstraction",

1 0

[GIT] ppl/ppl(master): References added.
by Patricia Hill 29 Dec '13

29 Dec '13

Module: ppl/ppl Branch: master Commit: 71413b47572fb435f2abb2f0e29925886975ce83 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=71413b47572f… Author: Patricia Hill <patricia.hill(a)bugseng.com> Date: Sun Dec 29 21:48:34 2013 +0000 References added. --- doc/ppl_citations.bib | 168 +++++++++++++++++++++++++++++++++++++----------- 1 files changed, 129 insertions(+), 39 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=71413b47…

1 0

[GIT] ppl/ppl(master): Several corrections to the abstract of Fu13th.
by Roberto Bagnara 29 Dec '13

29 Dec '13

Module: ppl/ppl Branch: master Commit: debbd4bf3e4b44a951b547a647d9d52cbe0c19e4 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=debbd4bf3e4b… Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com> Date: Sun Dec 29 17:26:25 2013 +0100 Several corrections to the abstract of Fu13th. --- doc/ppl_citations.bib | 12 ++++++------ 1 files changed, 6 insertions(+), 6 deletions(-) diff --git a/doc/ppl_citations.bib b/doc/ppl_citations.bib index deaa40f..5797b6f 100644 --- a/doc/ppl_citations.bib +++ b/doc/ppl_citations.bib @@ -2245,7 +2245,7 @@ Summarizing: Year = 2013, Abstract = "The fast and furious pace of change in computing technology has become an article of faith for many. The - reliability of computer-based systems cru- cially + reliability of computer-based systems crucially depends on the correctness of its computing. Can man, who created the computer, be capable of preventing machine-made misfortune? The theory of static analysis @@ -2253,24 +2253,24 @@ Summarizing: numerical properties of programs has been an essential research topic for static analysis. These kinds of properties are commonly modeled and handled by the - concept of numerical abstract domains. Unfor- tunately, + concept of numerical abstract domains. Unfortunately, lifting these domains to heap-manipulating programs is not obvious. On the other hand, points-to analyses have - been intensively studied to an- alyze pointer behaviors + been intensively studied to analyze pointer behaviors and some scale to very large programs but without inferring any numerical properties. We propose a framework based on the theory of abstract interpretation that is able to combine existing numerical domains and points-to analyses in a modular way. The static - numerical anal- ysis is prototyped using the SOOT + numerical analysis is prototyped using the SOOT framework for pointer analyses and the PPL library for numerical domains. The implementation is able to analyze large Java program within several minutes. The second part of this thesis consists of a theoretical study of - the com- bination of the points-to analysis with another + the combination of the points-to analysis with another pointer analysis providing information called must-alias. Two pointer variables must alias at some - pro- gram control point if they hold equal reference + program control point if they hold equal reference whenever the control point is reached. We have developed an algorithm of quadruple complexity that sharpens points-to analysis using must-alias information. The

1 0

[GIT] ppl/ppl(master): Added abstract of Fu13th.
by Roberto Bagnara 29 Dec '13

29 Dec '13

Module: ppl/ppl Branch: master Commit: 0032c63a93d8d7ca1330fb796d4c802f9766f1aa URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=0032c63a93d8… Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com> Date: Sun Dec 29 12:21:25 2013 +0100 Added abstract of Fu13th. --- doc/ppl_citations.bib | 58 ++++++++++++++++++++++++++++++++++++++---------- 1 files changed, 46 insertions(+), 12 deletions(-) diff --git a/doc/ppl_citations.bib b/doc/ppl_citations.bib index 9c0fa83..deaa40f 100644 --- a/doc/ppl_citations.bib +++ b/doc/ppl_citations.bib @@ -2233,6 +2233,52 @@ Summarizing: system benchmark from the literature." } +@PhDThesis{Fu13th, + Title = "Static Analysis of Numerical Properties in the Presence of Pointers", + Author = "Z. Fu", + Type = "Th\`{e}se pour le grade de + {``Docteur de l'Universit\'e de Rennes 1''}", + School = "\'{E}cole doctorale MATISSE, Universit\'{e} de Rennes 1 + sous le sceau de l'Universit\'e Europ\'eenne de Bretagne", + Address = "Rennes, France", + Month = dec, + Year = 2013, + Abstract = "The fast and furious pace of change in computing + technology has become an article of faith for many. The + reliability of computer-based systems cru- cially + depends on the correctness of its computing. Can man, + who created the computer, be capable of preventing + machine-made misfortune? The theory of static analysis + strives to achieve this ambition. The analysis of + numerical properties of programs has been an essential + research topic for static analysis. These kinds of + properties are commonly modeled and handled by the + concept of numerical abstract domains. Unfor- tunately, + lifting these domains to heap-manipulating programs is + not obvious. On the other hand, points-to analyses have + been intensively studied to an- alyze pointer behaviors + and some scale to very large programs but without + inferring any numerical properties. We propose a + framework based on the theory of abstract interpretation + that is able to combine existing numerical domains and + points-to analyses in a modular way. The static + numerical anal- ysis is prototyped using the SOOT + framework for pointer analyses and the PPL library for + numerical domains. The implementation is able to analyze + large Java program within several minutes. The second + part of this thesis consists of a theoretical study of + the com- bination of the points-to analysis with another + pointer analysis providing information called + must-alias. Two pointer variables must alias at some + pro- gram control point if they hold equal reference + whenever the control point is reached. We have developed + an algorithm of quadruple complexity that sharpens + points-to analysis using must-alias information. The + algorithm is proved correct following a semantics-based + formalization and the concept of bisimulation borrowed + from the game theory, model checking etc." +} + @Inproceedings{Fu14a, Author = "Z. Fu", Title = "Modularly Combining Numeric Abstract Domains with Points-to Analysis, and a Scalable Static Numeric Analyzer for Java", @@ -2285,18 +2331,6 @@ Summarizing: scalability." } -@PhDThesis{Fu13th, - Title = "Static Analysis of Numerical Properties in the Presence of Pointers", - Author = "Z. Fu", - Type = "Th\`{e}se pour le grade de - {``Docteur de l'Universit\'e de Rennes 1''}", - School = "\'{E}cole doctorale MATISSE, Universit\'{e} de Rennes 1 - sous le sceau de l'Universit\'e Europ\'eenne de Bretagne", - Address = "Rennes, France", - Month = dec, - Year = 2013, -} - @Article{GallardoP13, Author = "M.-d.-M. Gallardo and L. Panizo", Title = "Extending Model Checkers for Hybrid System Verification:

1 0

[GIT] ppl/ppl(master): Added Zu14th.
by Roberto Bagnara 29 Dec '13

29 Dec '13

Module: ppl/ppl Branch: master Commit: 077dd1051a9af69a1c9599f8e061de1c40f594fe URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=077dd1051a9a… Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com> Date: Sun Dec 29 12:15:59 2013 +0100 Added Zu14th. --- doc/ppl_citations.bib | 12 ++++++++++++ 1 files changed, 12 insertions(+), 0 deletions(-) diff --git a/doc/ppl_citations.bib b/doc/ppl_citations.bib index 3bbf21c..9c0fa83 100644 --- a/doc/ppl_citations.bib +++ b/doc/ppl_citations.bib @@ -2285,6 +2285,18 @@ Summarizing: scalability." } +@PhDThesis{Fu13th, + Title = "Static Analysis of Numerical Properties in the Presence of Pointers", + Author = "Z. Fu", + Type = "Th\`{e}se pour le grade de + {``Docteur de l'Universit\'e de Rennes 1''}", + School = "\'{E}cole doctorale MATISSE, Universit\'{e} de Rennes 1 + sous le sceau de l'Universit\'e Europ\'eenne de Bretagne", + Address = "Rennes, France", + Month = dec, + Year = 2013, +} + @Article{GallardoP13, Author = "M.-d.-M. Gallardo and L. Panizo", Title = "Extending Model Checkers for Hybrid System Verification:

1 0

[GIT] ppl/ppl(master): Added Fu14b.
by Roberto Bagnara 29 Dec '13

29 Dec '13

Module: ppl/ppl Branch: master Commit: 753472710977408c9937bf2951901b330840c13e URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=753472710977… Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com> Date: Sun Dec 29 12:04:28 2013 +0100 Added Fu14b. --- doc/ppl_citations.bib | 29 ++++++++++++++++++++++++++++- 1 files changed, 28 insertions(+), 1 deletions(-) diff --git a/doc/ppl_citations.bib b/doc/ppl_citations.bib index 4e47958..3bbf21c 100644 --- a/doc/ppl_citations.bib +++ b/doc/ppl_citations.bib @@ -2233,7 +2233,7 @@ Summarizing: system benchmark from the literature." } -@Inproceedings{Fu14, +@Inproceedings{Fu14a, Author = "Z. Fu", Title = "Modularly Combining Numeric Abstract Domains with Points-to Analysis, and a Scalable Static Numeric Analyzer for Java", Booktitle = "Verification, Model Checking, and Abstract Interpretation: @@ -2242,6 +2242,7 @@ Summarizing: Editor = "K. McMillan and X. Rival", Publisher = "Springer-Verlag, Berlin", Year = 2014, + Note = "To appear", Abstract = "This paper contributes to a new abstract domain that combines static numeric analysis and points-to analysis. One particularity of this abstract domain lies @@ -2258,6 +2259,32 @@ Summarizing: separately." } +@Inproceedings{Fu14b, + Author = "Z. Fu", + Title = "Targeted Update -- Aggressive Memory Abstraction Beyond Common + Sense and its Application on Static Numeric Analysis", + Booktitle = "Proceedings of the 23rd European Symposium on Programming + (ESOP'14)", + Address = "Grenoble, France", + Editor = "Z. Shao", + Publisher = "Springer-Verlag, Berlin", + Year = 2014, + Note = "To appear", + Abstract = "Summarizing techniques are widely used in the reasoning + of unbounded data structures. These techniques prohibit + strong update unless certain restricted safety + conditions are satisfied. We find that by setting and + enforcing the analysis boundaries to a limited scope of + program identifiers, called targets in this paper, more + cases of strong update can be shown sound, not with + regard to the entire heap, but with regard to the + targets. We have implemented the analysis for inferring + numeric properties in Java programs. The experimental + results show a tangible precision enhancement compared + with classical approaches while preserving high + scalability." +} + @Article{GallardoP13, Author = "M.-d.-M. Gallardo and L. Panizo", Title = "Extending Model Checkers for Hybrid System Verification:

1 0

[GIT] ppl/ppl(master): Several improvements.
by Roberto Bagnara 29 Dec '13

29 Dec '13

Module: ppl/ppl Branch: master Commit: 11b8475ea5b751cd65199563d7fd947cf26e10ab URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=11b8475ea5b7… Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com> Date: Sun Dec 29 11:41:21 2013 +0100 Several improvements. --- doc/ppl.bib | 4 ++-- doc/ppl_citations.bib | 20 ++++++++++++-------- 2 files changed, 14 insertions(+), 10 deletions(-) diff --git a/doc/ppl.bib b/doc/ppl.bib index 931706e..9374746 100644 --- a/doc/ppl.bib +++ b/doc/ppl.bib @@ -744,8 +744,8 @@ Summarizing: and the Double Description Method", Journal = "Formal Aspects of Computing", Publisher = "Springer-Verlag, London", - Volume = "17", - Number = "2", + Volume = 17, + Number = 2, Pages = "222--257", Year = 2005, ISSN = "0934-5043", diff --git a/doc/ppl_citations.bib b/doc/ppl_citations.bib index 32e3a39..4e47958 100644 --- a/doc/ppl_citations.bib +++ b/doc/ppl_citations.bib @@ -1016,7 +1016,7 @@ Summarizing: Publisher = "Springer-Verlag, Berlin", Series = "Lecture Notes in Computer Science", Volume = 5505, - Pages = "337-351", + Pages = "337--351", Year = 2009, ISBN = "978-3-642-00767-5", Abstract = "In this paper we prove that the transitive closure of a @@ -1307,7 +1307,7 @@ Summarizing: Booktitle = "Computer Aided Verification: Proceedings of the 25th International Conference (CAV 2013)", Year = 2013, - Pages = "511-526", + Pages = "511--526", Editor = "N. Sharygina and H. Veith", Publisher = "Springer-Verlag, Berlin", Series = "Lecture Notes in Computer Science", @@ -3837,11 +3837,14 @@ Summarizing: merely aim for precision." } -@Inproceedings{MontenegroSEP12, - Author = "M. Montenegro and O. Shkaravska and M. {van Eekelen} and R. Pe\~{n}a", - Title = "Interpolation-Based Height Analysis for Improving a Recurrence Solver", +@Incollection{MontenegroSEP12, + Author = "M. Montenegro and O. Shkaravska and M. {van Eekelen} + and R. Pe\~{n}a", + Title = "Interpolation-Based Height Analysis for Improving + a Recurrence Solver", Booktitle = "Foundational and Practical Aspects of Resource Analysis: - Second International Workshop, {FOPARA} 2011", + Second International Workshop (FOPARA 2011), + Revised Selected Papers", Editor = "R. Pe\~{n}a and M. {van Eekelen} and O. Shkaravska", Address = "Madrid, Spain", Pages = "36--53", @@ -4255,7 +4258,7 @@ Summarizing: Journal = "Bioinformatics", Publisher = "Oxford University Press", Volume = 25, - Number = "12", + Number = 12, Pages = "i169--i178", Year = 2009, Note = "Paper accepted for presentation at the 2009 ISMB/ECCB Conference, @@ -5197,7 +5200,8 @@ Summarizing: @Inproceedings{ZanioliFC12, Author = "M. Zanioli and P. Ferrara and A. Cortesi", Title = "{SAILS}: Static Analysis of Information Leakage with Sample", - Booktitle = "Proceedings of the 27th Annual {ACM} Symposium on Applied Computing", + Booktitle = "Proceedings of the 27th Annual ACM Symposium + on Applied Computing", Editor ="C.-C. Hung and J. Hong", Year = 2012, ISBN = "978-1-4503-0857-1",

1 0

[GIT] ppl/ppl(master): Abstracts fixed. Avoided non-ASCII characters.
by Roberto Bagnara 29 Dec '13

29 Dec '13

Module: ppl/ppl Branch: master Commit: 3ccd08df85d78ef507fd2a359251a009559fe110 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=3ccd08df85d7… Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com> Date: Sun Dec 29 11:01:13 2013 +0100 Abstracts fixed. Avoided non-ASCII characters. --- doc/ppl_citations.bib | 18 +++++++++--------- 1 files changed, 9 insertions(+), 9 deletions(-) diff --git a/doc/ppl_citations.bib b/doc/ppl_citations.bib index 9ef85bc..32e3a39 100644 --- a/doc/ppl_citations.bib +++ b/doc/ppl_citations.bib @@ -618,14 +618,14 @@ Summarizing: their complicated structures, quantitative time factors and even unknown delays. We present here PSyHCoS, a tool for analyzing parametric real-time systems - specied using the hierarchical modeling language + specified using the hierarchical modeling language PSTCSP. PSyHCoS supports several algorithms for parameter synthesis and model checking, as well as state space reduction techniques. Its architecture favors reusability in terms of syntax, semantics, and algorithms. It comes with a friendly user interface that can be used to edit, simulate and verify PSTCSP - models. Experiments show its eciency and + models. Experiments show its efficiency and applicability." } @@ -1178,7 +1178,7 @@ Summarizing: and J.~Ouaknine. and J.-F.~Raskin and J.~Worrell: On reachability for hybrid automata over bounded time. In: ICALP 2011, Part II. LNCS, vol. 6756, - pp. 416–427. Springer, Heidelberg (2011)] and show that + pp. 416-427. Springer, Heidelberg (2011)] and show that the problem is NExpTime-complete. We also show that we can effectively compute fixed points that characterise the sets of states that are reachable @@ -1401,7 +1401,7 @@ Summarizing: Booktitle = "Quantitative Evaluation of Systems: Proceedings of the 10th International Conference (QEST 2013)", Address = "Buenos Aires, Argentina", - Editor = "K. Joshi and M. Siegle and M. Stoelinga and P. R. D’Argenio", + Editor = "K. Joshi and M. Siegle and M. Stoelinga and P. R. D'Argenio", Year = 2013, Pages = "322--337", Publisher = "Springer-Verlag, Berlin", @@ -3202,8 +3202,8 @@ Summarizing: Abstract = "Geometric heuristics for the quantifier elimination approach presented by Kapur (2004) are investigated to automatically derive loop invariants expressing weakly - relational numerical properties (such as $l \leq x \leq h$ or - $l \leq \pm x \pm y \leq h)$ for imperative programs. + relational numerical properties (such as $l \leq x \leq h$ or + $l \leq \pm x \pm y \leq h)$ for imperative programs. Such properties have been successfully used to analyze commercial software consisting of hundreds of thousands of lines of @@ -3217,7 +3217,7 @@ Summarizing: approach has been generalized to consider disjunctive invariants of the similar form, expressed using maximum function (such as - $\max(x + a, y + b, z + c, d) \leq \max (x + e, y + f, z + g, h)$), + $\max(x+a, y+b, z+c, d) \leq \max (x+e, y+f, z+g, h)$), thus enabling automatic generation of a subclass of disjunctive invariants for imperative programs as well." } @@ -3472,7 +3472,7 @@ Summarizing: Year = 2013, ISBN = "978-3-319-02443-1 (Print) 978-3-319-02444-8 (Online)", Abstract = "PyEcdar is an open source implementation for reasoning - on timed systems. PyEcdar’s main objective is not + on timed systems. PyEcdar's main objective is not efficiency, but rather flexibility to test and implement new results on timed systems" } @@ -4566,7 +4566,7 @@ Summarizing: verification can be regarded as geometric concepts in machine learning. Safety properties define bad states: states a program should not reach. Program verification - explains why a program’s set of reachable states is + explains why a program's set of reachable states is disjoint from the set of bad states. In Hoare Logic, these explanations are predicates that form inductive assertions. Using samples for reachable and bad states

1 0