Showing cs.PLShow all
2 papers · 1 filter
cs.PL2024
Verifying Functional Correctness Properties At the Level of Java Bytecode
Marco Paganoni, Carlo A. Furia
The breakneck evolution of modern programming languages aggravates the development of deductive verification tools, which struggle to timely and fully support all new language feat…
cs.PL2024
Reasoning About Exceptional Behavior At the Level of Java Bytecode
Marco Paganoni, Carlo A. Furia
A program's exceptional behavior can substantially complicate its control flow, and hence accurately reasoning about the program's correctness. On the other hand, formally verifyin…