Preserving provability over GPU program optimizations with annotation-aware transformations [0.03%]
基于注解感知转换的GPU程序优化保真性研究
Ömer Şakar,Mohsen Safari,Marieke Huisman et al.
Ömer Şakar et al.
GPU programs are widely used in industry. To obtain the best performance, a typical development process involves the manual or semi-automatic application of optimizations prior to compiling the code. Such optimizations can introduce errors....
Martin Blicha,Konstantin Britikov,Natasha Sharygina
Martin Blicha
The logical framework of Constrained Horn Clauses (CHC) models verification tasks from a variety of domains, ranging from verification of safety properties in transition systems to modular verification of programs with procedures. In this w...
Raven Beutner,Bernd Finkbeiner
Raven Beutner
Temporal hyperproperties are system properties that relate multiple execution traces. In finite-state systems, temporal hyperproperties are supported by model-checking algorithms, and tools for general temporal logics like HyperLTL exist. I...
Information-flow interfaces [0.03%]
信息流界面
Ezio Bartocci,Thomas Ferrère,Thomas A Henzinger et al.
Ezio Bartocci et al.
Contract-based design is a promising methodology for taming the complexity of developing sophisticated systems. A formal contract distinguishes between assumptions, which are constraints that the designer of a component puts on the environm...
Practical algebraic calculus and Nullstellensatz with the checkers Pacheck and Pastèque and Nuss-Checker [0.03%]
实用的代数微积分和_Nullstellensatz_以及检查器Pacheck和Pastèque和Nuss-Checker
Daniela Kaufmann,Mathias Fleury,Armin Biere et al.
Daniela Kaufmann et al.
Automated reasoning techniques based on computer algebra have seen renewed interest in recent years and are for example heavily used in formal verification of arithmetic circuits. However, the verification process might contain errors. Gene...
Hari Govind Vediramana Krishnan,YuTing Chen,Sharon Shoham et al.
Hari Govind Vediramana Krishnan et al.
SMT-based model checkers, especially IC3-style ones, are currently the most effective techniques for verification of infinite state systems. They infer global inductive invariants via local reasoning about a single step of the transition re...
Isla: integrating full-scale ISA semantics and axiomatic concurrency models (extended version) [0.03%]
Isla：全面的ISA语义与公理式并发模型的整合（扩展版）
Alasdair Armstrong,Brian Campbell,Ben Simner et al.
Alasdair Armstrong et al.
Architecture specifications such as Armv8-A and RISC-V are the ultimate foundation for software verification and the correctness criteria for hardware verification. They should define the allowed sequential and relaxed-memory concurrency be...
Marcel Moosbrugger,Ezio Bartocci,Joost-Pieter Katoen et al.
Marcel Moosbrugger et al.
We describe the Amber tool for proving and refuting the termination of a class of probabilistic while-programs with polynomial arithmetic, in a fully automated manner. Amber combines martingale theory with properties of asymptotic bounding ...
Mathias Fleury,Armin Biere
Mathias Fleury
Bounded variable elimination is one of the most important preprocessing techniques in SAT solving. It benefits from discovering functional dependencies in the form of definitions encoded in the CNF. While the common approach pioneered in Sa...
Sepideh Asadi,Martin Blicha,Antti E J Hyvärinen et al.
Sepideh Asadi et al.
This article provides an innovative approach for verification by model checking of programs that undergo continuous changes. To tackle the problem of repeating the entire model checking for each new version of the program, our approach veri...