Verification, model checking, and abstract interpretation : 14th International Conference, VMCAI 2013, Rome, Italy, January 20-22, 2013. Proceedings /
Verification, model checking, and abstract interpretation : 14th International Conference, VMCAI 2013, Rome, Italy, January 20-22, 2013. Proceedings /
VMCAI 2013
Roberto Giacobazzi, Josh Berdine, Isabella Mastroeni (eds.).
- Berlin ; New York : Springer, ©2013.
- 1 online resource
- Lecture notes in computer science, 7737 0302-9743 ; Advanced research in computing and software science LNCS sublibrary. SL 1, Theoretical computer science and general issues .
- Lecture notes in computer science ; 7737. Lecture notes in computer science. Advanced research in computing and software science. LNCS sublibrary. SL 1, Theoretical computer science and general issues. .
Includes author index.
A Model-Constructing Satisfiability Calculus / Automata as Proofs / Complete Abstractions Everywhere / Abstraction-Guided Synthesis / Analysis of Systems with Continuous Behavior -- SMT-Based Bisimulation Minimisation of Markov Models / Hybrid Automata-Based CEGAR for Rectangular Hybrid Systems / Quantifying Information Leakage of Randomized Protocols / Synthesis -- Reductions for Synthesis Procedures / Towards Efficient Parameterized Synthesis / Leonardo de Moura, Dejan Jovanović -- Andreas Podelski -- Francesco Ranzato -- Eran Yahav -- Christian Dehnert, Joost-Pieter Katoen, David Parker -- Pavithra Prabhakar, Parasara Sridhar Duggirala, Sayan Mitra, Mahesh Viswanathan -- Fabrizio Biondi, Axel Legay, Pasquale Malacaria, Andrzej Wąsowski -- Swen Jacobs, Viktor Kuncak, Philippe Suter -- Ayrat Khalimov, Swen Jacobs, Roderick Bloem. Session 1: Session 2: Analysis Algorithms and Theorem Proving Techniques for Program Analysis -- Automatic Inference of Necessary Preconditions / Fixpoint Computation in the Polyhedra Abstract Domain Using Convex and Numerical Analysis Tools / SMT-Based Array Invariant Generation / Flow-Sensitive Fault Localization / Automata-Based Techniques -- Static Analysis of String Encoders and Decoders / Robustness Analysis of Networked Systems / Causality Checking for Complex System Models / Patrick Cousot, Radhia Cousot, Manuel Fähndrich, Francesco Logozzo -- Yassamine Seladji, Olivier Bouissou -- Daniel Larraz, Enric Rodríguez-Carbonell, Albert Rubio -- Jürgen Christ, Evren Ermis, Martin Schäf, Thomas Wies -- Loris D'Antoni, Margus Veanes -- Roopsha Samanta, Jyotirmoy V. Deshmukh, Swarat Chaudhuri -- Florian Leitner-Fischer, Stefan Leue. Session 3: Session 4: Tools -- ClabureDB: Classified Bug-Reports Database / Tool Integration with the Evidential Tool Bus / Types and Proof Methodologies -- Compositional and Lightweight Dependent Type Inference for ML / Abstract Read Permissions: Fractional Permissions without the Fractions / Types and Proof Methodologies -- Sound and Complete Flow Typing with Unions, Intersections and Negations / Abstract Domains -- Knockout Prediction for Reaction Networks with Partial Kinetic Information / Reduced Product Combination of Abstract Domains for Shapes / Abstraction of Syntax / Jiri Slaby, Jan Strejček, Marek Trtík -- Simon Cruanes, Gregoire Hamon, Sam Owre, Natarajan Shankar -- He Zhu, Suresh Jagannathan -- Stefan Heule, K. Rustan M. Leino, Peter Müller, Alexander J. Summers -- David J. Pearce -- Mathias John, Mirabelle Nebut, Joachim Niehren -- Antoine Toubhans, Bor-Yuh Evan Chang, Xavier Rival -- Vijay D'Silva, Daniel Kroening. Session 5: Session 6: Session 6: Session 7: Combining Boolean Solving and Abstract Domains for Theories -- Logico-Numerical Max-Strategy Iteration / A Constraint Solver Based on Abstract Domains / An Abstract Interpretation of DPLL(T) / Distributed/Concurrent System Verification -- All for the Price of Few / Uncovering Symmetries in Irregular Process Networks / State Space Reduction for Sensor Networks Using Two-Level Partial Order Reduction / Compositional Sequentialization of Periodic Programs / Peter Schrammel, Pavle Subotic -- Marie Pelleau, Antoine Miné, Charlotte Truchet, Frédéric Benhamou -- Martin Brain, Vijay D'Silva, Leopold Haller, Alberto Griggio, Daniel Kroening -- Parosh Aziz Abdulla, Frédéric Haziza, Lukáš Holík -- Kedar S. Namjoshi, Richard J. Trefler -- Manchun Zheng, David Sanán, Jun Sun, Yang Liu, Jin Song Dong, Yu Gu -- Sagar Chaki, Arie Gurfinkel, Soonho Kong, Ofer Strichman. Session 8: Session 9:
This book constitutes the refereed proceedings of the 14th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2013, held in Rome, Italy, in January 2013, co-located with the Symposium on Principles of Programming Languages, POPL 2013. The 27 revised full papers presented were carefully reviewed and selected from 72 submissions. The papers cover a wide range of topics including program verification, model checking, abstract interpretation and abstract domains, program synthesis, static analysis, type system, deductive methods, program certification, debugging techniques, program transformation, optimization, hybrid and cyber-physical systems.
9783642358739 364235873X 3642358721 9783642358722
Computer software--Verification--Congresses.
Software engineering--Congresses.
Software Validation
Software
Logiciels--Vérification--Congrès.
Génie logiciel--Congrès.
Logiciels--Validation.
Logiciels.
software.
COMPUTERS--Software Development & Engineering--Quality Assurance & Testing.
Computer software--Verification
Software engineering
Computer science. Computer Communication Networks. Software engineering. Logic design. Artificial intelligence. Logics and Meanings of Programs. Mathematical Logic and Formal Languages. Computation by Abstract Devices. computerwetenschappen computer sciences kunstmatige intelligentie wiskunde mathematics logica logic computational science computernetwerken computer networks Information and Communication Technology (General) Informatie- en communicatietechnologie (algemeen)
Congress
proceedings (reports)
Conference papers and proceedings
Conference papers and proceedings.
Actes de congrès.
QA76.76.V47 / V53 2013
005.1/4
QA 76.76.V47
Includes author index.
A Model-Constructing Satisfiability Calculus / Automata as Proofs / Complete Abstractions Everywhere / Abstraction-Guided Synthesis / Analysis of Systems with Continuous Behavior -- SMT-Based Bisimulation Minimisation of Markov Models / Hybrid Automata-Based CEGAR for Rectangular Hybrid Systems / Quantifying Information Leakage of Randomized Protocols / Synthesis -- Reductions for Synthesis Procedures / Towards Efficient Parameterized Synthesis / Leonardo de Moura, Dejan Jovanović -- Andreas Podelski -- Francesco Ranzato -- Eran Yahav -- Christian Dehnert, Joost-Pieter Katoen, David Parker -- Pavithra Prabhakar, Parasara Sridhar Duggirala, Sayan Mitra, Mahesh Viswanathan -- Fabrizio Biondi, Axel Legay, Pasquale Malacaria, Andrzej Wąsowski -- Swen Jacobs, Viktor Kuncak, Philippe Suter -- Ayrat Khalimov, Swen Jacobs, Roderick Bloem. Session 1: Session 2: Analysis Algorithms and Theorem Proving Techniques for Program Analysis -- Automatic Inference of Necessary Preconditions / Fixpoint Computation in the Polyhedra Abstract Domain Using Convex and Numerical Analysis Tools / SMT-Based Array Invariant Generation / Flow-Sensitive Fault Localization / Automata-Based Techniques -- Static Analysis of String Encoders and Decoders / Robustness Analysis of Networked Systems / Causality Checking for Complex System Models / Patrick Cousot, Radhia Cousot, Manuel Fähndrich, Francesco Logozzo -- Yassamine Seladji, Olivier Bouissou -- Daniel Larraz, Enric Rodríguez-Carbonell, Albert Rubio -- Jürgen Christ, Evren Ermis, Martin Schäf, Thomas Wies -- Loris D'Antoni, Margus Veanes -- Roopsha Samanta, Jyotirmoy V. Deshmukh, Swarat Chaudhuri -- Florian Leitner-Fischer, Stefan Leue. Session 3: Session 4: Tools -- ClabureDB: Classified Bug-Reports Database / Tool Integration with the Evidential Tool Bus / Types and Proof Methodologies -- Compositional and Lightweight Dependent Type Inference for ML / Abstract Read Permissions: Fractional Permissions without the Fractions / Types and Proof Methodologies -- Sound and Complete Flow Typing with Unions, Intersections and Negations / Abstract Domains -- Knockout Prediction for Reaction Networks with Partial Kinetic Information / Reduced Product Combination of Abstract Domains for Shapes / Abstraction of Syntax / Jiri Slaby, Jan Strejček, Marek Trtík -- Simon Cruanes, Gregoire Hamon, Sam Owre, Natarajan Shankar -- He Zhu, Suresh Jagannathan -- Stefan Heule, K. Rustan M. Leino, Peter Müller, Alexander J. Summers -- David J. Pearce -- Mathias John, Mirabelle Nebut, Joachim Niehren -- Antoine Toubhans, Bor-Yuh Evan Chang, Xavier Rival -- Vijay D'Silva, Daniel Kroening. Session 5: Session 6: Session 6: Session 7: Combining Boolean Solving and Abstract Domains for Theories -- Logico-Numerical Max-Strategy Iteration / A Constraint Solver Based on Abstract Domains / An Abstract Interpretation of DPLL(T) / Distributed/Concurrent System Verification -- All for the Price of Few / Uncovering Symmetries in Irregular Process Networks / State Space Reduction for Sensor Networks Using Two-Level Partial Order Reduction / Compositional Sequentialization of Periodic Programs / Peter Schrammel, Pavle Subotic -- Marie Pelleau, Antoine Miné, Charlotte Truchet, Frédéric Benhamou -- Martin Brain, Vijay D'Silva, Leopold Haller, Alberto Griggio, Daniel Kroening -- Parosh Aziz Abdulla, Frédéric Haziza, Lukáš Holík -- Kedar S. Namjoshi, Richard J. Trefler -- Manchun Zheng, David Sanán, Jun Sun, Yang Liu, Jin Song Dong, Yu Gu -- Sagar Chaki, Arie Gurfinkel, Soonho Kong, Ofer Strichman. Session 8: Session 9:
This book constitutes the refereed proceedings of the 14th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2013, held in Rome, Italy, in January 2013, co-located with the Symposium on Principles of Programming Languages, POPL 2013. The 27 revised full papers presented were carefully reviewed and selected from 72 submissions. The papers cover a wide range of topics including program verification, model checking, abstract interpretation and abstract domains, program synthesis, static analysis, type system, deductive methods, program certification, debugging techniques, program transformation, optimization, hybrid and cyber-physical systems.
9783642358739 364235873X 3642358721 9783642358722
Computer software--Verification--Congresses.
Software engineering--Congresses.
Software Validation
Software
Logiciels--Vérification--Congrès.
Génie logiciel--Congrès.
Logiciels--Validation.
Logiciels.
software.
COMPUTERS--Software Development & Engineering--Quality Assurance & Testing.
Computer software--Verification
Software engineering
Computer science. Computer Communication Networks. Software engineering. Logic design. Artificial intelligence. Logics and Meanings of Programs. Mathematical Logic and Formal Languages. Computation by Abstract Devices. computerwetenschappen computer sciences kunstmatige intelligentie wiskunde mathematics logica logic computational science computernetwerken computer networks Information and Communication Technology (General) Informatie- en communicatietechnologie (algemeen)
Congress
proceedings (reports)
Conference papers and proceedings
Conference papers and proceedings.
Actes de congrès.
QA76.76.V47 / V53 2013
005.1/4
QA 76.76.V47