LEVY
发表于 2025-3-25 06:40:01
Practical Abstractions for Automated Verification of Shared-Memory Concurrency,e its reliability. To be able to reason about realistic programs, these techniques must be modular and compositional as well as practical by being supported by automated tools. However, many existing approaches for concurrency verification are theoretical and focus on expressivity and generality. Th
lethargy
发表于 2025-3-25 08:04:29
http://reply.papertrans.cn/99/9818/981737/981737_22.png
plasma
发表于 2025-3-25 14:58:25
Witnessing Secure Compilation,validated independently with a refinement checker. This process is illustrated for common optimizations. Crucially, it is not necessary to formally verify the compiler implementation, which is infeasible for production compilers.
展览
发表于 2025-3-25 18:14:08
The Correctness of a Code Generator for a Functional Language, a simple first-order functional language with arrays. We exhibit a bisimulation between the functional execution and the imperative execution. This bisimulation shows that the generated imperative program returns the same result as the functional program.
Institution
发表于 2025-3-25 22:03:38
Cheap CTL Compassion in NuSMV,culus embedding requires only alternation depth two, the resulting specifications correspond to parity games with two priorities. This allows a comparison of the performance of our . with existing parity game solvers (both explicit and symbolic). The advantages of the symbolic approach seem to extend to fair model checking.
单纯
发表于 2025-3-26 03:38:12
http://reply.papertrans.cn/99/9818/981737/981737_26.png
surmount
发表于 2025-3-26 05:31:28
http://reply.papertrans.cn/99/9818/981737/981737_27.png
CLOUT
发表于 2025-3-26 11:54:52
Promptness and Bounded Fairness in Concurrent and Parameterized Systems,utoff results for different classes of systems with a parametric number of components and quantitative specifications, thereby identifying previously unknown decidable fragments of the parameterized model checking problem.
Asparagus
发表于 2025-3-26 12:50:00
Solving , Using Approximations,emand under and over-approximations of . formulas, it can avoid the space overhead that is integral to previous approaches. We have implemented our procedure in a prototype and report on encouraging results that suggest that . formulas can be checked for satisfiability without computing a prohibitively large equivalent Presburger formula.
Felicitous
发表于 2025-3-26 19:03:40
http://reply.papertrans.cn/99/9818/981737/981737_30.png