Alk Platform

Alk is an educational platform designed for writing, executing, and analyzing algorithms. The platform consists of an algorithmic language, an interpreter able to execute algorithms, and tools to understand, analyze, and evaluate algorithms, and to acquire rigorous algorithm thinking.

What inputs are supported?

Annotated algorithms.

For which programming languages does it support?

Alk language, a very simple dynamic typed algorithmic language.

What properties can be verified?

Properties like loop invariants, contracts, for algorithms or pieces of algorithms.

What are the tool’s main techniques for the supported (input, property) pairs?

The verification process is via Matching Logic [1,2] and symbolic execution [3].

What external tools are used? (e.g., compilers, SMT solvers)

Now, it uses the Z3 prover in the backend.

What is the tool’s URL?

https://github.com/alk-language/java-semantics

Example(s)

@havoc a : array<int>;
slp = 1;
i = 1;
@assume a.size() > 0;
@assume forall i : int :: 0 <= i && i < a.size() - 1 ==> a[i] <= a[i + 1];
while (i < a.size())
@invariant 1 <= slp && i <= a.size();
@invariant (exists k:int :: slp - 1 <= k && k < i && a[k] == a[k - slp + 1]);
@modifies slp, i;
{
    if (a[i] == a[i - slp])
        slp = slp + 1;
    i = i + 1;
}

References

1. Xiaohong Chen, Dorel Lucanu, Grigore Rosu: Matching logic explained. J. Log. Algebraic Methods Program. 120, 2021, https://www.sciencedirect.com/science/article/abs/pii/S2352220821000018?via%3Dihub
2. Lungu, A., Lucanu, D.: A matching logic foundation for Alk. In: Seidl, H., Liu, Z., Pasareanu, C.S. (eds.) Theoretical Aspects of Computing - ICTAC 2022 - 19th International Colloquium, Tbilisi, Georgia, September 27-29, 2022, Proceedings. Lecture Notes in Computer Science, vol. 13572, pp. 290–304. Springer (2022). https://doi.org/10.1007/978-3-031-17715-6“ ̇19
3. Lungu, A., Lucanu, D.: Supporting algorithm analysis with symbolic execution in Alk. In: Ameur, Y.A., Craciun, F. (eds.) Theoretical Aspects of Software Engineering - 16th International Symposium, TASE 2022, Proceedings. Lecture Notes in Computer Science, vol. 13299, pp. 406–423. Springer (2022), https://doi.org/10.1007/978-3-031-10363-6 27