10 citations · 28 across the 8 of their papers we have counts for
8 papers
S2TD: a Separation Logic Verifier that Supports Reasoning of the Absence and Presence of Bugs
Quang Loc Le, Jun Sun, Long H. Pham +1
Heap-manipulating programs are known to be challenging to reason about. We present a novel verifier for heap-manipulating programs called S2TD, which encodes programs systematicall…
Automated Modular Verification for Race-Free Channels with Implicit and Explicit Synchronization
Andreea Costea, Wei-Ngan Chin, Florin Craciun +1
Ensuring the correctness of software for communication centric programs is important but challenging. Previous approaches, based on session types, have been intensively investigate…
Automated Verification of CountDownLatch
Wei-Ngan Chin, Ton Chanh Le, Shengchao Qin
The CountDownLatch (CDL) is a versatile concurrency mechanism that was first introduced in Java 5, and is also being adopted into C++ and C#. Its usage allows one or more threads t…
Enhancing Symbolic Execution of Heap-based Programs with Separation Logic for Test Input Generation
Long H. Pham, Quang Loc Le, Quoc-Sang Phan +2
Symbolic execution is a well established method for test input generation. Despite of having achieved tremendous success over numerical domains, existing symbolic execution techniq…
Toward `verifying' a Water Treatment System
Jingyi Wang, Jun Sun, Yifan Jia +2
Modeling and verifying real-world cyber-physical systems is challenging, which is especially so for complex systems where manually modeling is infeasible. In this work, we report o…
Automatically 'Verifying' Discrete-Time Complex Systems through Learning, Abstraction and Refinement
Jingyi Wang, Jun Sun, Shengchao Qin +1
Precisely modeling complex systems like cyber-physical systems is challenging, which often render model-based system verification techniques like model checking infeasible. To over…
MDM: A Mode Diagram Modeling Framework
Zheng Wang, Geguang Pu, Jianwen Li +5
Periodic control systems used in spacecrafts and automotives are usually period-driven and can be decomposed into different modes with each mode representing a system state observe…
MDM: A Mode Diagram Modeling Framework for Periodic Control Systems
Zheng Wang, Geguang Pu, Shenchao Qin +5
Periodic control systems used in spacecrafts and automotives are usually period-driven and can be decomposed into different modes with each mode representing a system state observe…