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
        }
    }
}

Assured Automatic Programming via Large Language Models

Published in arXiv preprint, 2024

This paper proposes an approach for combining large language model code generation with formal assurance, so that automatically generated programs come with correctness guarantees.

Recommended citation: M. Mirchev, A. Costea, A. K. Singh, A. Roychoudhury. (2024). "Assured Automatic Programming via Large Language Models." arXiv preprint.

Share on

Twitter Facebook LinkedIn

Martin Mirchev

Share on