A Sound and Correct Formalism to Specify, Verify and Synthesize Behavior in BIG DATA Systems. - Fernando Asteasuain; Luciana Rodriguez Caldeira (CACIC, 2021)