Formal Verification

Automatically finding atomic regions for fixing bugs in Concurrent Programs

This paper presents a technique for automatically constructing a fix for buggy concurrent programs: given a concurrent program that does not satisfy user-provided assertions, we infer atomic blocks that fix the program. An atomic block protects a …

Underspecified harnesses and interleaved bugs

This paper presents a technique to find interleaved bugs even with incomplete harness.

Reactivity in SystemC Transaction-Level Models

SystemC is a popular language used in modeling system-on-chip implementations. To support this task at a high level of abstraction, transaction-level modeling (TLM) libraries have been recently developped. While TLM libraries are useful, it is …