00:00:00 / 00:00:00
1 5

Relational tight field bounds for distributed analysis of programs

By Marcelo Frias

Relational tight field bounds are an abstraction of the semantics of data structures. In the presence of appropriate symmetry-breaking predicates, these bounds can be computed automatically and allow to dramatically speed up bug-finding using SAT- solving. In this lecture, after giving an introduction to tight field bounds and symmetry- breaking predicates, I will present a general technique for distributing program analyses. As examples, I will show how the technique allows one to distribute SAT-based bug-finding as well as symbolic execution over complex data types.

Information about the video

Citation data

  • DOI 10.24350/CIRM.V.19827503
  • Cite this video Frias, Marcelo (03/11/2021). Relational tight field bounds for distributed analysis of programs. CIRM. Audiovisual resource. DOI: 10.24350/CIRM.V.19827503
  • URL https://dx.doi.org/10.24350/CIRM.V.19827503

Domain(s)

Bibliography

  • GALEOTTI, Juan P., ROSNER, Nicolás, POMBO, Carlos G. López, et al. TACO: Efficient SAT-based bounded verification using symmetry breaking and tight bounds. IEEE Transactions on Software Engineering, 2013, vol. 39, no 9, p. 1283-1307. - https://doi.org/10.1109/TSE.2013.15
  • ROSNER, Nicolás, GALEOTTI, Juan, BERMÚDEZ, Santiago, et al. Parallel bounded analysis in code with rich invariants by refinement of field bounds. In : Proceedings of the 2013 International Symposium on Software Testing and Analysis. 2013. p. 23-33. - https://doi.org/10.1145/2483760.2483770

Last related questions on MathOverflow

You have to connect your Carmin.tv account with mathoverflow to add question

Ask a question on MathOverflow




Register

  • Bookmark videos
  • Add videos to see later &
    keep your browsing history
  • Comment with the scientific
    community
  • Get notification updates
    for your favorite subjects
Give feedback