Incremental design-space model checking via reusable reachable state approximations

DOI10.1007/S10703-022-00389-5zbMath1492.68085OpenAlexW3127122249WikidataQ114226449 ScholiaQ114226449MaRDI QIDQ2149964

Rohit Dureja, Kristin Yvonne Rozier

Publication date: 27 June 2022

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://lib.dr.iastate.edu/cgi/viewcontent.cgi?article=1181&context=aere_pubs

zbMATH Keywords

model checkingreachability analysisair traffic controldesign-space explorationincremental verification

Mathematics Subject Classification ID

Application models in control theory (93C95) Traffic problems in operations research (90B20) Specification and verification (program logics, model checking, etc.) (68Q60) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Uses Software

• MathSAT5

Cites Work

• Unnamed Item
• Coverage metrics for temporal logic model checking
• Min-wise independent permutations
• Incremental bounded model checking for embedded software
• More scalable LTL model checking via discovering design-space dependencies \((D^3)\)
• Infinite-state invariant checking with IC3 and predicate abstraction
• Understanding IC3
• Interpolant Learning and Reuse in SAT-Based Model Checking
• SAT-Based Model Checking without Unrolling
• The MathSAT5 SMT Solver
• Computer Aided Verification

This page was built for publication: Incremental design-space model checking via reusable reachable state approximations