149 citations · 1.2k across the 55 of their papers we have counts for
5 papers · 1 filter
Practical Range Refinement Types with Inference
Valentin Aebi, Carlo A. Furia
Refinement types are a static verification technique that aims at increasing the expressivity of traditional type systems while remaining easy and natural to use. While systems bas…
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…
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…
Challenges of Multilingual Program Specification and Analysis
Carlo A. Furia, Abhishek Tiwari
Multilingual programs, whose implementations are made of different languages, are gaining traction especially in domains, such as web programming, that particularly benefit from th…
C to O-O Translation: Beyond the Easy Stuff
Marco Trudel, Carlo A. Furia, Martin Nordio +2
Can we reuse some of the huge code-base developed in C to take advantage of modern programming language features such as type safety, object-orientation, and contracts? This paper…