Name
Abstract | ||
|---|---|---|
•We formalize the notion of assignments and assignment strategies.•We present an SMT encoding from which assignment strategies are extracted.•We define a sound decomposition of a TLA+ formula into symbolic transitions.•We implement the above as part of the APALACHE model checker.•We present experimental results using several state-of-the-art TLA+ specifications. |
Year | DOI | Venue |
|---|---|---|
2020 | 10.1016/j.scico.2019.102361 | Science of Computer Programming |
Keywords | Field | DocType |
TLA+,SMT,Symbolic transition systems | Programming language,Computer science | Journal |
Volume | ISSN | Citations |
187 | 0167-6423 | 0 |
PageRank | References | Authors |
0.34 | 0 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Jure Kukovec | 1 | 0 | 0.34 |
| Thanh-Hai Tran | 2 | 33 | 12.51 |
| Igor Konnov | 3 | 57 | 12.06 |