An ongoing challenge for computer science is the development of a tool which automatically verifies programs meet their specifications, and are free from runtime errors such as divide-by-zero, array out-of-bounds and null dereferences. We have been developing a programming language from scratch to simplify verification, called Whiley, and an accompanying verifying compiler. Like other modern programming languages (e.g. Go, Rust) Whiley eschews ideas from object orientation and is perhaps most similar in style to C. In this paper, we illustrate a short example illustrating how C strings can be encoded in Whiley, and then safely reasoned about.
Tue 27 OctDisplayed time zone: Eastern Time (US & Canada) change
10:30 - 12:00
|Beyond Bash: Shell scripting in a statically-typed, object-oriented language|
|Rust: Idioms and Design Patterns|
Nicholas Cameron Mozilla Research
|Whiley: a Better C?|
David J. Pearce Victoria University of WellingtonLink to publication