Information Technology Reference
In-Depth Information
property, it may provide a strong hint at the desired data structure. Therefore, it
is reasonable to use the current data structure as the starting point for finding the
value that satisfies the desired constraint, hoping that the correct data structure
is close to the current one. Although such approach is slightly more natural in
the context of imperative than functional code, it is relevant whenever the data
manipulated is large enough. The first specification-driven approach for data
structure repair is by Demsky and Rinard [18,19] where the goal is to recover
from corrupted data structures by transforming states that are erroneous with
respect to integrity constraints into valid ones, performing local heuristic search.
Subsequent work uses less custom constraint solvers instead [21,22]. We believe
that SMT solvers could also play a role in this domain. Researchers [77] have
also used method contracts instead of data structure integrity constraints to be
able to support rich behavioral specifications, which makes it also more relevant
for our scenarios. While the primary goal in most works is run-time recovery of
data structures, recent work [44] extends the technique for debugging purposes,
by abstracting concrete repair actions to program statements performing the
same actions. As in general for run-time constraint solving, we expect that data
structure repair can be productively applied to implementations generated using
“speculative synthesis” that generates a not necessarily correct implementation.
References
1. Ait-Kaci, H.: Warren's Abstract Machine: A Tutorial Reconstruction. MIT Press
(1991)
2. Antoy, S.: Definitional trees. In: ALP, pp. 143-157 (1992)
3. Antoy, S., Hanus, M.: Functional logic programming. CACM 53(4), 74-85 (2010)
4. Asarin, E., Maler, O., Pnueli, A.: Symbolic controller synthesis for discrete and
timed systems. In: Hybrid Systems II, pp. 1-20 (1995)
5. Back, R.-J., von Wright, J.: In: Refinement Calculus, Springer (1998)
6.Barnett,M,Chang,B.-Y.E,DeLine,R,Jacobs,B,Leino,K.R.M:Boogie:
A modular reusable verifier for object-oriented programs. In: de Boer, F.S.,
Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111,
pp. 364-387. Springer, Heidelberg (2006)
7. Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded model
checking. Advances in Computers 58 (2003)
8. Bierman, G.M., Gordon, A.D., Hritcu, C., Langworthy, D.E.: Semantic subtyping
with an SMT solver. In: ICFP, pp. 105-116 (2010)
9. Blanc, R.W., Kneuss, E., Kuncak, V., Suter, P.: An overview of the Leon verification
system: Verification by translation to recursive functions. In: Scala Workshop (2013)
10. Bodden, E., Lam, P., Hendren, L.J.: Partially evaluating finite-state runtime mon-
itors ahead of time. ACM Trans. Program. Lang. Syst. 34(2), 7 (2012)
11. Braßel, B., Hanus, M., Muller, M.: High-level database programming in Curry.
In: Hudak, P., Warren, D.S. (eds.) PADL 2008. LNCS, vol. 4902, pp. 316-332.
Springer, Heidelberg (2008)
12. Bruynooghe, M., Schreye, D.D., Krekels, B.: Compiling control. The Journal of
Logic Programming 6(12), 135-162 (1989)
13. Butler, M., Grundy, J., Langbacka, T., Ruksenas, R., von Wright, J.: The refinement
calculator: Proof support for program refinement. In: Formal Methods Pacific (1997)
