Experiences porting the jikes RVM to Linux/IA32
Bowen Alpern, María Butrico, et al.
JAVA VM 2002
An approach to proving temporal properties of concurrent programs that does not use temporal logic as an inference system is presented. The approach is based on using Buchi automata to specify properties. To show that a program satisfies a given property, proof obligations are derived from the Buchi automata specifying that property. These obligations are discharged by devising suitable invariant assertions and variant functions for the program. The approach is shown to be sound and relatively complete. A mutual exclusion protocol illustrates its application. © 1989, ACM. All rights reserved.
Bowen Alpern, María Butrico, et al.
JAVA VM 2002
Bowen Alpern, Alan Carle, et al.
ACM SIGPLAN Notices
Jennifer Widom, David Gries, et al.
ACM Transactions on Programming Languages and Systems (TOPLAS)
Bowen Alpern, Joshua Auerbach, et al.
VEe 2005