TY - GEN
T1 - Proving correctness of JavaCard DL taclets using Bali
AU - Trentelman, Kerry
PY - 2005
Y1 - 2005
N2 - Developed at the University of Karlsruhe, KeY is an augmented commercial CASE tool with specification and deductive verification functionalities. Recently, lightweight, stand-alone tactics or «taclets» have been introduced in order to implement the JavaCard dynamic logic (JavaCard DL) sequent calculus within KeY. JavaCard DL captures the semantics of JavaCard, the subset of Java designed to run on smart cards. This paper discusses a case-study into proving taclets sound using the independent Bali formalism of Java in the theorem prover Isabelle/HOL. Rather than taking a foundational approach by embedding the entire JavaCard DL semantics directly into a theorem prover, we instead translate each taclet and prove its soundness via the Bali calculus. We analyse both calculi, prove three pivotal taclets sound, and argue whether the method is useful in proving the correctness of JavaCard programs overall.
AB - Developed at the University of Karlsruhe, KeY is an augmented commercial CASE tool with specification and deductive verification functionalities. Recently, lightweight, stand-alone tactics or «taclets» have been introduced in order to implement the JavaCard dynamic logic (JavaCard DL) sequent calculus within KeY. JavaCard DL captures the semantics of JavaCard, the subset of Java designed to run on smart cards. This paper discusses a case-study into proving taclets sound using the independent Bali formalism of Java in the theorem prover Isabelle/HOL. Rather than taking a foundational approach by embedding the entire JavaCard DL semantics directly into a theorem prover, we instead translate each taclet and prove its soundness via the Bali calculus. We analyse both calculi, prove three pivotal taclets sound, and argue whether the method is useful in proving the correctness of JavaCard programs overall.
UR - http://www.scopus.com/inward/record.url?scp=38849145555&partnerID=8YFLogxK
U2 - 10.1109/SEFM.2005.37
DO - 10.1109/SEFM.2005.37
M3 - Conference contribution
SN - 0769524354
SN - 9780769524351
T3 - Proceedings - 3rd IEEE International Conference on Software Engineering and Formal Methods, SEFM 2005
SP - 160
EP - 169
BT - Proceedings - 3rd IEEE International Conference on Software Engineering and Formal Methods, SEFM 2005
T2 - 3rd IEEE International Conference on Software Engineering and Formal Methods, SEFM 2005
Y2 - 7 September 2005 through 9 September 2005
ER -