CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Deductive Search for Errors in Free Data Type Specifications using Model Generation

Wolfgang Ahrendt (Institutionen för datavetenskap)
Lecture Notes in Computer Science. 18th International Conference on Automated Deduction Copenhagen, Denmark, July 27–30, 2002 (0302-9743). Vol. 2392 (2002), p. 211-225.
[Konferensbidrag, refereegranskat]

The presented approach aims at identifying false conjectures about free data types. Given a specification and a conjecture, the method performs a search for a model of an according counter specification. The model search is tailor-made for the semantical setting of free data types, where the fixed domain allows to describe models just in terms of interpretations. For sake of interpretation construction, a theory specific calculus is provided. The concrete rules are ‘executed’ by a procedure known as model generation. As most free data types have infinite domains, the ability of automatically solving the non-consequence problem is necessarily limited. That problem is addressed by limiting the instantiation of the axioms. This approximation leads to a restricted notion of model correctness, which is discussed. At the same time, it enables model completeness for free data types, unlike approaches based on limiting the domain size.



Denna post skapades 2013-01-14.
CPL Pubid: 170475

 

Läs direkt!


Länk till annan sajt (kan kräva inloggning)


Institutioner (Chalmers)

Institutionen för datavetenskap (2002-2004)

Ämnesområden

Data- och informationsvetenskap

Chalmers infrastruktur