Lab for Automated Reasoning and Analysis LARA

Lecture 14: Logics for Data Structures: BAPA and WS1S

Continuing Lecture 13

BAPA

WS1S

(Jahob demos for combination of SPASS, MONA, BAPA to prove ListSize.java

Need for Reachability

Weak Monadic Logic of One Successor

References

 
sav10/lecture_14.txt · Last modified: 2010/05/11 20:59 by vkuncak
 
© EPFL 2018 - Legal notice