### Skapa referens, olika format (klipp och klistra)

**Harvard**

Claessen, K. och Svensson, H. (2008) *Finding Counter Examples in Induction Proofs*.

** BibTeX **

@conference{

Claessen2008,

author={Claessen, Koen and Svensson, Hans},

title={Finding Counter Examples in Induction Proofs},

booktitle={Proceedings of the 2nd International Conference on Tests and Proofs, in the LNCS series of Springer},

abstract={This paper addresses a problem arising in automated proof of invariants of transition systems, for example transition systems modelling distributed programs. Most of the time, the actual properties we want to prove are too weak
to hold inductively, and auxiliary invariants need to be introduced. The problem is how to find these extra invariants. We propose a method where we find minimal counter examples to candidate invariants by means of automated random testing techniques. These counter examples can be inspected by a human user, and used to adapt the set of invariants at hand. We are able to find two different kinds of counter examples, either indicating (1) that the used invariants are too strong (a concrete trace of the system violates at least one of the invariants), or (2) that the used invariants are too weak (a concrete
transition of the system does not maintain all invariants). We have developed and evaluated our method in the context of formally verifying an industrial-strength implementation of a fault-tolerant distributed leader election protocol.
},

year={2008},

}

** RefWorks **

RT Conference Proceedings

SR Print

ID 69236

A1 Claessen, Koen

A1 Svensson, Hans

T1 Finding Counter Examples in Induction Proofs

YR 2008

T2 Proceedings of the 2nd International Conference on Tests and Proofs, in the LNCS series of Springer

AB This paper addresses a problem arising in automated proof of invariants of transition systems, for example transition systems modelling distributed programs. Most of the time, the actual properties we want to prove are too weak
to hold inductively, and auxiliary invariants need to be introduced. The problem is how to find these extra invariants. We propose a method where we find minimal counter examples to candidate invariants by means of automated random testing techniques. These counter examples can be inspected by a human user, and used to adapt the set of invariants at hand. We are able to find two different kinds of counter examples, either indicating (1) that the used invariants are too strong (a concrete trace of the system violates at least one of the invariants), or (2) that the used invariants are too weak (a concrete
transition of the system does not maintain all invariants). We have developed and evaluated our method in the context of formally verifying an industrial-strength implementation of a fault-tolerant distributed leader election protocol.

LA eng

OL 30