Fast Infinite-State Model Checking in Integer-Based Systems

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


Duration: 1:17:58
80 views
0

In this talk we discuss the use of logic for reachability analysis for infinite-state systems. Infinite-state systems are formalised using transition systems over a first-order structure. We establish a common ground relating a large class of algorithms by analysing the connections between the symbolic representation of transition systems and formulas used in various reachability algorithms. We consider in detail the so-called guarded assignment systems and local reachability algorithms. We show how an implementation of local reachability algorithms and a new incremental algorithm for finding Hilbert's base in the system BRAIN resulted in much faster reachability checking than in systems using constraint libraries and decision procedures for Presburger's arithmetic. Experimental results demonstrate that problems in protocol verification which are beyond the reach of other existing systems can be solved completely automatically. (Joint work with Tatiana Rybina)



Other Videos By Microsoft Research


2016-09-05Structure and stability of complex networks.
2016-09-05Confronting Reality: Doing What Matters to Get Things Done Right
2016-09-05Recent Developments in Linguistics -- And in the UW Department of Linguistics
2016-09-05Dartmouth Digital Dorm          
2016-09-05A CLP Approach to Modelling Systems
2016-09-05Dynamosaics: Dynamic Mosaics with Non-Chronological Time
2016-09-05Automatic Failure Diagnosis in Large-Scale Systems
2016-09-05The Economics of Software Dependability
2016-09-05An Overview of Recent CMU Research on Model-Based Face Processing
2016-09-05Resource acquisition via an unsupervised WSD system
2016-09-05Fast Infinite-State Model Checking in Integer-Based Systems
2016-09-05WeΓÇÖre Friends, Right?: Inside KidsΓÇÖ Culture [1/4]
2016-09-05Accelerated Democracy: How technology might change voting
2016-09-05When Can Formal Methods Make a Real Difference?
2016-09-05Dynamic Semantics of Programming Languages and Applications to Testing
2016-09-05Error Detection using Shape Analysis with Local Reasoning
2016-09-05Type-Safe, Generative, Binding Macros
2016-09-05Social Network Analysis meets the Semantic Web: What FOAF Reveals About LiveJournal
2016-09-05Distributed Multi-robot Exploration and Mapping
2016-09-051.Vision: Extraordinary Computing Experiences & 2. Robots for the Masses: Fiction or Reality
2016-09-05Modeling and Facilitating Human Communication [1/5]


Tags:
microsoft research