scientific article; zbMATH DE number 7589540
From MaRDI portal
Publication:5866353
DOI10.18255/1818-1015-550-571zbMath1497.68316MaRDI QIDQ5866353
Dmitriĭ Aleksandrovich Mordvinov
Publication date: 21 September 2022
Full work available at URL: http://mathnet.ru/eng/mais697
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)
Uses Software
Cites Work
- SMT-based model checking for recursive programs
- Program invariants as fixedpoints
- Relational verification through Horn clause transformation
- Relational program reasoning using compiler IR
- Regression verification for unbalanced recursive functions
- Infinite-state invariant checking with IC3 and predicate abstraction
- Generalized Property Directed Reachability
- SAT-Based Model Checking without Unrolling
- Synchronizing Constrained Horn Clauses
- Exploiting synchrony and symmetry in relational verification
- HoIce: an ICE-based non-linear Horn clause solver