1

This paper describes a sound and complete tool, 2LS, for program verification and the techniques behind its working.

This paper introduces Re-Order Bounded Model Checking to efficiently repair programs on weak memory models.

This paper describes techniques to incremental encode cardinality constraints. This led Open-WBO to win accolades in MaxSAT evaluations.

This paper presents a technique to perform May-Happen-in-Parallel analysis for languages with Dynamic Barriers.

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

Static assertion checking of open programs requires setting up a precise harness to capture the environment assumptions. For instance, a library may require a file handle to be properly initialized before it is passed into it. A harness is used to …

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 …