AutoHyper: Explicit-state model checking for HyperLTL
R Beutner, B Finkbeiner - … Conference on Tools and Algorithms for the …, 2023 - Springer
HyperLTL is a temporal logic that can express hyperproperties, ie, properties that relate
multiple execution traces of a system. Such properties are becoming increasingly important …
multiple execution traces of a system. Such properties are becoming increasingly important …
ALASCA: reasoning in quantified linear arithmetic
Automated reasoning is routinely used in the rigorous construction and analysis of complex
systems. Among different theories, arithmetic stands out as one of the most frequently used …
systems. Among different theories, arithmetic stands out as one of the most frequently used …
Refining Unification with Abstraction
Automated reasoning with theories and quantifiers is a common demand in formal methods.
A major challenge that arises in this respect comes with rewriting/simplifying terms that are …
A major challenge that arises in this respect comes with rewriting/simplifying terms that are …
[图书][B] Tools and Algorithms for the Construction and Analysis of Systems: 29th International Conference, TACAS 2023, Held as Part of the European Joint …
S Sankaranarayanan, N Sharygina - 2023 - library.oapen.org
This open access book constitutes the proceedings of the 29th International Conference on
Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2023, which was …
Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2023, which was …
[PDF][PDF] G a*, _2 bQMBM; BM Zm MiB} 2/GBM2Bi? K2iB+ U1ti2M/2/o2bBQMV
Automated reasoningisroutinelyusedin therigorousconstruction and analysis of complex
systems. Among different theories, arithmetic stands out as one of the most frequently used …
systems. Among different theories, arithmetic stands out as one of the most frequently used …