11 citations · 14 across the 6 of their papers we have counts for
7 papers
Staged Specification Logic for Verifying Higher-Order Imperative Programs (Technical Report)
Darius Foo, Yahui Song, Wei-Ngan Chin
Higher-order functions and imperative states are language features supported by many mainstream languages. Their combination is expressive and useful, but complicates specification…
Tracing OCaml Programs
Darius Foo, Wei-Ngan Chin
This presentation will cover a framework for application-level tracing of OCaml programs. We outline a solution to the main technical challenge, which is being able to log typed va…
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…
Automated Lemma Synthesis in Symbolic-Heap Separation Logic
Quang-Trung Ta, Ton Chanh Le, Siau-Cheng Khoo +1
The symbolic-heap fragment of separation logic has been actively developed and advocated for verifying the memory-safety property of computer programs. At present, one of its bigge…
UStore: A Distributed Storage With Rich Semantics
Anh Dinh, Ji Wang, Sheng Wang +9
Today's storage systems expose abstractions which are either too low-level (e.g., key-value store, raw-block store) that they require developers to re-invent the wheels, or too hig…
Automated Mutual Explicit Induction Proof in Separation Logic
Quang-Trung Ta, Ton Chanh Le, Siau-Cheng Khoo +1
We present a sequent-based deductive system for automatically proving entailments in separation logic by using mathematical induction. Our technique, called mutual explicit inducti…