method Max(a: int, b: int)
returns (m: int)
ensures m >= a && m >= b
ensures m == a || m == b
{
if a >= b { m := a; }
else { m := b; }
}
predicate Sorted(s: seq<int>)
{
forall i, j ::
0 <= i < j < |s| ==>
s[i] <= s[j]
}
method BinarySearch(a: array<int>,
key: int)
returns (index: int)
requires Sorted(a[..])
ensures 0 <= index ==>
a[index] == key
ensures index < 0 ==>
forall k ::
0 <= k < a.Length ==>
a[k] != key
{
var lo, hi := 0, a.Length;
while lo < hi
invariant 0 <= lo <= hi
{
var mid := (lo + hi) / 2;
if a[mid] < key {
lo := mid + 1;
} else if key < a[mid] {
hi := mid;
} else {
return mid;
}
}
return -1;
}
lemma MaxCommutative(a: int, b: int)
ensures Max(a, b) == Max(b, a)
{
}
fn verify(x: &State) -> bool {
x.balance >= 0
&& x.locked <= x.balance
}
#[requires(n > 0)]
#[ensures(ret >= n)]
fn next_pow2(n: u64) -> u64 {
let mut p = 1;
while p < n {
p <<= 1;
}
p
}
(declare-const x Int)
(declare-const y Int)
(assert (> x 0))
(assert (= (+ x y) 10))
(check-sat)
; sat
(get-model)
; (define-fun x () Int 3)
; (define-fun y () Int 7)
(assert (forall ((a Int) (b Int))
(=> (and (> a 0) (> b 0))
(> (+ a b) 0))))
(check-sat)
; unsat
impl Repair for Patch {
fn verify(&self) -> Outcome {
if self.tests_pass()
&& self.no_regression() {
Outcome::Plausible
} else {
Outcome::Rejected
}
}
}
PhD student at the National University of Singapore, working in the Programming Languages and Software Engineering (PLSE) Lab within the Trustworthy Software Systems group under Professor Abhik Roychoudhury. My research spans automated program repair, automated verified evolution of software systems, and AI-assisted software security.