Ultimate Automizer with an On-Demand Construction of Floyd-Hoare Automata

被引：13

作者：

Heizmann, Matthias ^{[1
]}

Chen, Yu-Wen ^{[1
]}

Dietsch, Daniel ^{[1
]}

Greitschus, Marius ^{[1
]}

Nutz, Alexander ^{[1
]}

Musa, Betim ^{[1
]}

Schaetzle, Claus ^{[1
]}

Schilling, Christian ^{[1
]}

Schuessele, Frank ^{[1
]}

Podelski, Andreas ^{[1
]}

机构：

[1] Univ Freiburg, Freiburg, Germany

来源：

TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, TACAS 2017, PT II | 2017年 / 10206卷

关键词：

D O I：

10.1007/978-3-662-54580-5_30

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

ULTIMATE AUTOMIZER is a software verifier that implements an automata-based approach for the verification of safety and liveness properties. A central new feature that speeded up the abstraction refinement of the tool is an on-demand construction of Floyd-Hoare automata.

引用

页码：394 / 398

页数：5

共 32 条

[1] FLOYD-HOARE LOGIC IN ITERATION THEORIES
BLOOM, SL
ESIK, Z
[J]. JOURNAL OF THE ACM, 1991, 38 (04) : 887 - 934
[2] Floyd-Hoare Logic for Quantum Programs
Ying, Mingsheng
[J]. ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2011, 33 (06):
[3] Inference Systems for Floyd-Hoare Logic with Partial Predicates
Nikitchenko, Mykola
Kryvolap, Andrii
[J]. INFORMATICS 2013: PROCEEDINGS OF THE TWELFTH INTERNATIONAL CONFERENCE ON INFORMATICS, 2013, : 88 - 93
[4] A General Framework for Sound and Complete Floyd-Hoare Logics
Arthan, Rob
Martin, Ursula
Mathiesen, Erik A.
Oliva, Paulo
[J]. ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2009, 11 (01)
[5] Extended Floyd-Hoare Logic over Relational Nominative Data
Nikitchenko, Mykola
Ivanov, Ievgen
Kornilowicz, Artur
Kryvolap, Andrii
[J]. INFORMATION AND COMMUNICATION TECHNOLOGIES IN EDUCATION, RESEARCH, AND INDUSTRIAL APPLICATIONS, ICTERI 2017, 2018, 826 : 41 - 64
[6] An Inference System of an Extension of Floyd-Hoare Logic for Partial Predicates
Ivanov, Ievgen
Kornilowicz, Artur
Nikitchenko, Mykola
[J]. FORMALIZED MATHEMATICS, 2018, 26 (02): : 159 - 164
[7] Deriving a Floyd-Hoare logic for non-local jumps from a formulae-as-types notion of control
Crolard, T.
Polonowski, E.
[J]. JOURNAL OF LOGIC AND ALGEBRAIC PROGRAMMING, 2012, 81 (03): : 181 - 208
[8] A Floyd-Warshall-based Reoptimization of Q Matrix on the Single DVRPPD with On-demand Cancellations
Catapang, Jasper Kyle
Solano, Geoffrey A.
[J]. 12TH INTERNATIONAL CONFERENCE ON ICT CONVERGENCE (ICTC 2021): BEYOND THE PANDEMIC ERA WITH ICT CONVERGENCE INNOVATION, 2021, : 172 - 177
[9] InstantGrid: A framework for on-demand grid point construction
Ho, RSC
Yin, KK
Lee, DCM
Hung, DHF
Wang, CL
Lau, FCM
[J]. GRID AND COOPERATIVE COMPUTING GCC 2004, PROCEEDINGS, 2004, 3251 : 911 - 914
[10] Parallel On-Demand Hierarchy Construction on Contemporary GPUs
Vinkler, Marek
Havran, Vlastimil
Bittner, Jiri
Sochor, Jiri
[J]. IEEE TRANSACTIONS ON VISUALIZATION AND COMPUTER GRAPHICS, 2016, 22 (07) : 1886 - 1898

← 1 2 3 4 →