19th International Conference on Relational and Algebraic Methods in Computer Science / 19ème Conférence internationale de méthodes relationnelles et algébriques en informatique

Collection 19th International Conference on Relational and Algebraic Methods in Computer Science / 19ème Conférence internationale de méthodes relationnelles et algébriques en informatique

Organizer(s) Fahrenberg, Uli ; Gehrke, Mai ; Santocanale, Luigi ; Winter, Michael

Date(s) 02/11/2021 - 06/11/2021

linked URL https://conferences.cirm-math.fr/2398.html

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

Date of recording 03/11/2021
Date of publication 26/11/2021
Institution CIRM
Licence CC BY NC ND
Language English
Audience Researchers
Director(s) Luca Recanzone
Format MP4

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)

Computer Science

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

MSC codes

Document(s)

https://www.cirm-math.fr/RepOrga/2398/Slides/Frias.pdf

Last related questions on MathOverflow

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

Ask a question on MathOverflow

All the collection videos

01:03:09

published on November 26, 2021

Relational tight field bounds for distributed analysis of programs

By Marcelo Frias

44:23

published on November 26, 2021

Quantified constraint satisfaction problem: towards the classification of complexity

By Dmitriy Zhuk

25:24

published on November 26, 2021

Time warps, from algebra to algorithms

By Simon Santschi

01:00:52

published on November 26, 2021

Fixpoint games

By Barbara König

29:45

published on November 26, 2021

Relational models for the Lambek calculus with intersection and unit

By Stepan Kuznetsov

Copyright Carmin.tv 2024

Give feedback