Automated technology for verification and analysis : 13th International Symposium, ATVA 2015, Shanghai, China, October 12-15, 2015, Proceedings /: 13th International Symposium, ATVA 2015, Shanghai, China, October 12-15, 2015, Proceedings. (2015)

• Record Type: Book
• Other Titles: ATVA 2015
• Further Information: Note: Bernd Finkbeiner, Geguang Pu, Lijun Zhang (eds.).
• Editors: Finkbeiner, Bernd; Pu, G (Geguang); Zhang, Lijun, 1979-
• Other Names: ATVA (Symposium), 13th
• Contents: Intro; Preface; Organization; Contents; Probabilistic Programming: A True Verification Challenge; References; Machines Reasoning About Machines: 2015; 1 Introduction; 2 A Quick History and Acknowledgments; 3 1970s -- Simple List Processing; 4 1980s -- Academic Math and Computer Science; 5 1990s -- Commercial Breakthrough; 6 2000s -- Gradual Acceptance; 7 2010 -- Integrated with the Design Process; 8 Lessons; 9 Conclusion; References; Using SMT for Solving Fragments of Parameterised Boolean Equation Systems; 1 Introduction; 2 Preliminaries; 3 A Motivating Example 4 Disjunctive and Conjunctive PBESs5 Solving Disjunctive and Conjunctive PBESs Using SMT; 5.1 Finding Lasso-Shaped Proof Graphs; 5.2 Proving the Absence of Proof Graphs; 5.3 A Pseudo-Decision Procedure; 6 Experiments; 7 Closing Remarks; References; Unfolding-Based Process Discovery; 1 Introduction; 2 Preliminaries; 3 Independence-Preserving Discovery; 4 Introducing Generalization; 4.1 Language-Preserving Generalization; 4.2 Controlling Generalization via Negative Information; 5 Computing Folding Equivalences; 5.1 SMT Encoding; 5.2 Finding an Optimal Folding Equivalence; 6 Experiments 7 Related Work8 Conclusions; References; Improving Interpolants for Linear Arithmetic; 1 Introduction; 2 Preliminaries; 2.1 Notations; 2.2 Computing Interpolants by Resolution Proofs; 2.3 Computing Interpolants by DC-Removability Checks; 2.4 Description of a State Set; 3 The General Algorithm; 3.1 Test Whether One Additional Linear Constraint Is Sufficient; 3.2 Finding Pairs of Indistinguishable Points with SMT; 3.3 Enlarge Pairs of Indistinguishable Points to Convex Regions; 3.4 Finding a Linear Constraint Separating Pairs of Convex Regions with LP; 4 Optimizations; 5 Experimental Results 6 Conclusion and Further ResearchReferences; A Mechanically Checked Generation of Correlating Programs Directed by Structured Syntactic Differences; 1 Introduction; 2 Overview; 3 Source Language and Its Guarded Form; 3.1 Input Language; 3.2 Guarded Language; 3.3 Translation to Guarded Form; 4 Structured Differences Between Programs; 5 Generation Algorithm Directed by Structured Differences; 6 Implementation and Experiments; 7 Related Work; 8 Conclusion; References; On Automated Lemma Generation for Separation Logic with Inductive Definitions; 1 Introduction; 2 Motivating Example 3 Separation Logic with Inductive Definitions4 Composition Lemmas; 5 Derived Lemmas; 5.1 The ``Completion'' Lemmas; 5.2 The ``Stronger'' Lemmas; 6 A Proof Strategy Based on Lemmas; 7 Experimental Results; 8 Related Work; 9 Conclusion; References; Severity Levels of Inconsistent Code; 1 Introduction; 2 Overview; 3 Inconsistent Code; 4 Severity Levels of Inconsistency; 5 Algorithm for Categorizing Inconsistent Code; 6 Evaluation; 7 Related Work; 8 Conclusion; References; Learning the Language of Error; 1 Introduction; 2 Preliminaries -- the L* Algorithm; 3 The Language We Learn
• Publisher Details: Cham : Springer
• Publication Date: 2015
• Extent: 1 online resource (xiii, 520 pages), illustrations
• Subjects: 006.3/33; Computer science; Automatic theorem proving -- Congresses; Artificial intelligence -- Congresses; Artificial intelligence; Automatic theorem proving; Computer Science; Engineering & Applied Sciences; Computer Science; Programming Languages, Compilers, Interpreters; Logics and Meanings of Programs; Mathematical Logic and Formal Languages; Artificial Intelligence (incl. Robotics); Programming Techniques; Computers -- Programming -- General; Mathematics -- Logic; Computers -- Intelligence (AI) & Semantics; Computer programming / software development; Mathematical theory of computation; Artificial intelligence; Logic design; Artificial intelligence; Computers -- Programming Languages -- General; Programming & scripting languages: general; Electronic books; Conference papers and proceedings; Electronic books
• Languages: English
• ISBNs: 9783319249537; 3319249533
• Related ISBNs: 9783319249520; 3319249525
• Notes: Note: Online resource; title from PDF title page (SpringerLink, viewed December 14, 2015).
• Access Rights: Legal Deposit; Only available on premises controlled by the deposit library and to one user at any one time; The Legal Deposit Libraries (Non-Print Works) Regulations (UK).
• Access Usage: Restricted: Printing from this resource is governed by The Legal Deposit Libraries (Non-Print Works) Regulations (UK) and UK copyright law currently in force.