Open Access. Powered by Scholars. Published by Universities.®
Articles 1 - 2 of 2
Full-Text Articles in Computer Engineering
Parasol: Efficient Parallel Synthesis Of Large Model Spaces, Clay Stevens, Hamid Bagheri
Parasol: Efficient Parallel Synthesis Of Large Model Spaces, Clay Stevens, Hamid Bagheri
CSE Conference and Workshop Papers
Formal analysis is an invaluable tool for software engineers, yet state-of-the-art formal analysis techniques suffer from well-known limitations in terms of scalability. In particular, some software design domains—such as tradeoff analysis and security analysis—require systematic exploration of potentially huge model spaces, which further exacerbates the problem. Despite this present and urgent challenge, few techniques exist to support the systematic exploration of large model spaces. This paper introduces Parasol, an approach and accompanying tool suite, to improve the scalability of large-scale formal model space exploration. Parasol presents a novel parallel model space synthesis approach, backed with unsupervised learning to automatically derive …
Combining Solution Reuse And Bound Tightening For Efficient Analysis Of Evolving Systems, Clay Stevens, Hamid Bagheri
Combining Solution Reuse And Bound Tightening For Efficient Analysis Of Evolving Systems, Clay Stevens, Hamid Bagheri
CSE Conference and Workshop Papers
Software engineers have long employed formal verification to ensure the safety and validity of their system designs. As the system changes—often via predictable, domain-specific operations—their models must also change, requiring system designers to repeatedly execute the same formal verification on similar system models. State-of-the-art formal verification techniques can be expensive at scale, the cost of which is multiplied by repeated analysis. This paper presents a novel analysis technique—implemented in a tool called SoRBoT—which can automatically determine domain-specific optimizations that can dramatically reduce the cost of repeatedly analyzing evolving systems. Different from all prior approaches, which focus on either tightening the …