EmergenTheta: Verification Beyond Abstraction Refinement (Competition Contribution)

Bajczi, Levente ✉ [Bajczi, Levente (informatika), szerző] Méréstechnika és Információs Rendszerek Tanszék (BME / VIK); Kritikus Rendszerek Kutatócsoport (BME / VIK / MIT); Szekeres, Dániel [Szekeres, Dániel (informatika), szerző] Méréstechnika és Információs Rendszerek Tanszék (BME / VIK); Kritikus Rendszerek Kutatócsoport (BME / VIK / MIT); Mondok, Milán [Mondok, Milán (informatika), szerző] Méréstechnika és Információs Rendszerek Tanszék (BME / VIK); Kritikus Rendszerek Kutatócsoport (BME / VIK / MIT); Ádám, Zsófia [Ádám, Zsófia (informatika), szerző] Méréstechnika és Információs Rendszerek Tanszék (BME / VIK); Kritikus Rendszerek Kutatócsoport (BME / VIK / MIT); Somorjai, Márk [Somorjai, Márk (Informatika), szerző] Kritikus Rendszerek Kutatócsoport (BME / VIK / MIT); Telbisz, Csanád [Telbisz, Csanád Ferenc (informatika), szerző] Méréstechnika és Információs Rendszerek Tanszék (BME / VIK); Kritikus Rendszerek Kutatócsoport (BME / VIK / MIT); Dobos-Kovács, Mihály [Dobos-Kovács, Mihály (informatika), szerző] Méréstechnika és Információs Rendszerek Tanszék (BME / VIK); Kritikus Rendszerek Kutatócsoport (BME / VIK / MIT); Molnár, Vince [Molnár, Vince (informatika), szerző] Méréstechnika és Információs Rendszerek Tanszék (BME / VIK); Kritikus Rendszerek Kutatócsoport (BME / VIK / MIT)

Angol nyelvű Konferenciaközlemény (Folyóiratcikk) Tudományos
Megjelent: LECTURE NOTES IN COMPUTER SCIENCE 0302-9743 1611-3349 14572 pp. 371-375 Paper: Chapter 23 2024
Konferencia: 30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2024, which was held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024 2024-04-06 [Luxembourg, Luxemburg]
    Theta is a model checking framework conventionally based on abstraction refinement techniques. While abstraction is useful for a large number of verification problems, the over-reliance on the technique led to Theta being unable to meaningfully adapt. Identifying this problem in previous years of SV-COMP has led us to create EmergenTheta , a sandbox for the new approaches we want Theta to support. By differentiating between mature and emerging techniques, we can experiment more freely without hurting the reliability of the overall framework. In this paper we detail the development route to EmergenTheta , and its first debut on SV-COMP’24 in the ReachSafety category.
    Hivatkozás stílusok: IEEEACMAPAChicagoHarvardCSLMásolásNyomtatás
    2025-02-07 05:23