Embedded systems often come with constrained memory footprints. It is therefore essential to ensure that software running on such platforms fulfils memory usage specifications at c...
TAPAAL is a new platform independent tool for modelling, simulation and verification of timed-arc Petri nets. TAPAAL provides a stand-alone editor and simulator, while the verifica...
We present a framework for certifying hardware designs generated through behavioral synthesis, by using formal verification to certify the associated synthesis transformations. We ...
Sandip Ray, Kecheng Hao, Yan Chen, Fei Xie, Jin Ya...
Abstract. As Service-Oriented Architectures are more widely adopted, it becomes more important to adopt measures for ensuring that the services satisfy functional and non-functiona...
We present specification languages that naturally capture exactly the regular and -regular properties that are stutter invariant. Our specification languages are variants of the cl...
Code model checking is a rapidly advancing research topic. However, apart from very constrained scenarios (e.g., verification of device drivers by Slam), the code model checking t...
Abstract. We present a new method for fighting the state space explosion of process algebraic specifications, by performing static analysis on an intermediate format: linear proc...
Abstract. A distributed system is fault-tolerant if it continues to perform correctly even when a subset of the processes becomes faulty. Faulttolerance is highly desirable but oft...