<pre>The goal of PLPV is to foster and stimulate research at the intersection of programming languages and program verification, by bringing together experts from diverse areas like types, contracts, interactive theorem proving, model checking and program analysis. Work in this area typically attempts to reduce the burden of program verification by taking advantage of particular semantic or structural properties of the programming language. Examples include dependently typed programming languages, which leverage a language′s type system to specify and check richer than usual specifications, possibly with programmer–provided proof terms, extended static checking systems like ESC/Java and Spec#, which incorporate contracts and static contract verifiers. We invite submissions on all aspects, both theoretical and practical, of the integration of programming language and program verification technology. To encourage cross–pollination between different communities, we seek a broad the scope for PLPV. In particular, submissions may have diverse foundations for verification (Type–based, Hoare–logic–based, Abstract Interpretation–based, etc), target different kinds of programming languages (functional, imperative, object–oriented, etc), and apply to diverse kinds of program properties (data structure invariants, security properties, temporal protocols, resource constraints, etc). </pre>
Abbrevation
PLPV
City
Austin
Country
United States
Deadline Paper
Start Date
End Date
Abstract