白杨鱼
发表于 2025-3-30 11:36:22
Program Verification Under Weak Memory Consistency Using Separation Logict separation logic, we develop a number of sound program logics for fragments of the C/C++11 memory model. We show that these logics are useful not only for verifying concurrent programs, but also for explaining the weak memory constructs of C/C++.
龙卷风
发表于 2025-3-30 12:43:26
http://reply.papertrans.cn/24/2334/233386/233386_52.png
Laconic
发表于 2025-3-30 19:17:14
http://reply.papertrans.cn/24/2334/233386/233386_53.png
SENT
发表于 2025-3-30 22:27:06
Program Verification Under Weak Memory Consistency Using Separation Logic1 or Java) or by the hardware architecture (e.g., for assembly and legacy C code). Since most work in concurrent software verification has been developed prior to weak memory consistency, it is natural to ask how these models affect formal reasoning about concurrent programs..In this overview paper,
召集
发表于 2025-3-31 01:48:57
The Power of Symbolic Automata and Transducerstheories, such as linear arithmetic. Therefore, these models extend their classic counterparts to operate over infinite alphabets, such as the set of rational numbers. Due to their expressiveness, symbolic automata and transducers have been used to verify functional programs operating over lists and
etiquette
发表于 2025-3-31 05:42:28
Maximum Satisfiability in Software Analysis: Applications and Techniquesthe Maximum Satisfiability (MaxSAT) problem, an optimization extension of the Boolean Satisfiability (SAT) problem. We demonstrate the approach on three diverse applications that advance the state-of-the-art in balancing tradeoffs in software analysis. Enabling these applications on real-world progr
Brittle
发表于 2025-3-31 11:46:12
Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networksg them to safety-critical systems is the great difficulty in providing formal guarantees about their behavior. We present a novel, scalable, and efficient technique for verifying properties of deep neural networks (or providing counter-examples). The technique is based on the simplex method, extende
主动
发表于 2025-3-31 17:13:18
Automated Recurrence Analysis for Almost-Linear Expected-Runtime Boundsvation is that several classical textbook algorithms have quite efficient expected-runtime complexity, whereas the corresponding worst-case bounds are either inefficient (e.g., .), or completely ineffective (e.g., .). Since the main focus of expected-runtime analysis is to obtain efficient bounds, w
Bmd955
发表于 2025-3-31 20:25:31
http://reply.papertrans.cn/24/2334/233386/233386_59.png
Ibd810
发表于 2025-3-31 22:03:14
Ensuring the Reliability of Your Model Checker: Interval Iteration for Markov Decision Processesmerical results that it returns is critical. However, recent results have shown that implementations of value iteration, a widely used iterative numerical method for computing reachability probabilities, can return results that are incorrect by several orders of magnitude. To remedy this, interval i