enter search term and/or author name
Affine Refinement Types for Secure Distributed Programming
Michele Bugliesi, Stefano Calzavara, Fabienne Eigner, Matteo Maffei
Article No.: 11
Recent research has shown that it is possible to leverage general-purpose theorem-proving techniques to develop powerful type systems for the verification of a wide range of security properties on application code. Although successful in many...
Polyhedral AST Generation Is More Than Scanning Polyhedra
Tobias Grosser, Sven Verdoolaege, Albert Cohen
Article No.: 12
Abstract mathematical representations such as integer polyhedra have been shown to be useful to precisely analyze computational kernels and to express complex loop transformations. Such transformations rely on abstract syntax tree (AST) generators...
Behavioral Subtyping, Specification Inheritance, and Modular Reasoning
Gary T. Leavens, David A. Naumann
Article No.: 13
Verification of a dynamically dispatched method call, E.m(), seems to depend on E’s dynamic type. To avoid case analysis and allow incremental development, object-oriented program verification uses supertype abstraction....