ABD 1: Property-based verification

The first paper is about the static analysis of constraints that define the environment of an IP, typically a communication protocol, and guarantee that the environment is not over-constrained. The second paper presents the use of affine arithmetic to model typical properties of mixed-signal devices and check the impact of parameter deviations on the system behavior. The third contribution discusses the use of verified CTL properties about a system components to generate efficient component abstractions and verify a global property on their composition.