[CSUSB]>> [CNS]>> [CSE]>> [R J Botting]>> biba.php
Bibliographic Item (1.0)
- Patrice Chalin
- Engineering a sound assertion semantics for the verifying compiler
- IEEE Trans Software Engineering V36n2(Mar/Apr 2010)pp275-287
- =TYPE USER V&V SQA FORMAL METHOD TOOL VC VERIFICATION COMPILER
- A verifying compiler should spot when assertions will go wrong.
- The logic of the verifying compiler should allow for expressions being undefined.
- Must handle arithmetic errors like 1/0 correctly. Even in assertions!
- Stresses the need to talk to the users of the compiler before deciding its semantics!
- Introduces a definedness predicate.
- Formal Methods shouldn't have imposed an elegant but unsound logic on software.
Search for bibliographic items containing a matching string.
Search for a specific bibliographic item by name.
To see the complete bibliography (1Mb+) select:[Bibliography]