Model-Checking Modulo Theories: Declarative Framework and Pragmatic Issues

Channel:
Microsoft Research
Subscribers:
344,000
Published on ● Video Link: https://www.youtube.com/watch?v=NhK3y6WidiY


Duration: 1:10:56
102 views
1

We discuss the notion of array-based system as a suitable abstraction of infinite state systems such as parametrised systems or sorting programs. By using a class of quantified-first order formulae to symbolically represent array-based systems, we propose methods to check safety (invariance) properties on top of Satisfiability Modulo Theories (SMT) solvers. We identify hypotheses under which such verification technique becomes a decision procedure for invariance properties of array-based systems and discuss the difficulties to make the approach viable in practice. In this respect, the use of quantified first-order formulae to describe sets of states makes checking for fix-point and unsafety extremely expensive. Thus, we focus on (static and dynamic) techniques for instance reduction and illustrate some experimental results of our implementation of the framework in the MCMT model-checker.



Other Videos By Microsoft Research


2016-09-07Automated reasoning in non-classical logics with the polarized inverse method
2016-09-07Where computer vision needs help from computer science
2016-09-07Parallel Programming with Chorus
2016-09-07Seeing Software
2016-09-07Efficient and Effective File Replication and Consistency Maintenance in P2P Systems
2016-09-07Where to Go: Interpreting Natural Directions Using Global Inference
2016-09-07Algorithms Meet Art, Puzzles, and Magic
2016-09-07Free: The Future of a Radical Price
2016-09-07Provably-Efficient Adaptive Scheduling with Parallelism Feedback
2016-09-07Personal Health Information among Competing Public Goods
2016-09-07Model-Checking Modulo Theories: Declarative Framework and Pragmatic Issues
2016-09-07Theory Tea Meeting Talk: On Local Dynamics for Two Equilibrium Concepts
2016-09-07Finding Loop Invariants Using a Theorem Prover
2016-09-07Bandwidth Allocation in TCP Friendliness and P2P Streaming
2016-09-07Improving the Development of Interactive Software Through New Language Features and Patterns
2016-09-07Better Multiple Intents Re-ranking
2016-09-07Verifying the Interplay of Authorization Policies and Workflow in Service-Oriented Architectures
2016-09-07Twig: A Simple, AI-friendly, Character World for Believable Agents
2016-09-07Speech signals separation with microphone array
2016-09-07NxOpinion: A Novel Integrated and Predictive Solution for Global Healthcare Delivery
2016-09-07Improving Software Production Environments with Non-Invasive, Quantitative Experience Collection


Tags:
microsoft research