Loading...
Please wait, while we are loading the content...
Similar Documents
Rewriting modulo smt
| Content Provider | NASA Technical Reports Server (NTRS) |
|---|---|
| Author | Munoz, Cesar A. Meseguer, Jose Rocha, Camilo |
| Copyright Year | 2013 |
| Description | Combining symbolic techniques such as: (i) SMT solving, (ii) rewriting modulo theories, and (iii) model checking can enable the analysis of infinite-state systems outside the scope of each such technique. This paper proposes rewriting modulo SMT as a new technique combining the powers of (i)-(iii) and ideally suited to model and analyze infinite-state open systems; that is, systems that interact with a non-deterministic environment. Such systems exhibit both internal non-determinism due to the system, and external non-determinism due to the environment. They are not amenable to finite-state model checking analysis because they typically are infinite-state. By being reducible to standard rewriting using reflective techniques, rewriting modulo SMT can both naturally model and analyze open systems without requiring any changes to rewriting-based reachability analysis techniques for closed systems. This is illustrated by the analysis of a real-time system beyond the scope of timed automata methods. |
| File Size | 482814 |
| Page Count | 25 |
| File Format | |
| Alternate Webpage(s) | http://archive.org/details/NASA_NTRS_Archive_20140002750 |
| Archival Resource Key | ark:/13960/t23c11z7s |
| Language | English |
| Publisher Date | 2013-08-01 |
| Access Restriction | Open |
| Subject Keyword | Computer Programming And Software Computer Programming Automata Theory Automatic Control Computer Systems Programs Multiprocessing Computers Real Time Operation Ntrs Nasa Technical Reports ServerĀ (ntrs) Nasa Technical Reports Server Aerodynamics Aircraft Aerospace Engineering Aerospace Aeronautic Space Science |
| Content Type | Text |
| Resource Type | Technical Report |