Using formal verification to evaluate the execution time of Spark applications

DOI10.1007/s00165-020-00505-4zbMath1451.68166OpenAlexW3009390554WikidataQ131112945 ScholiaQ131112945MaRDI QIDQ782497

Gaetano Quattrocchi, Matteo Rossi, Marcello M. Bersani, F. Marconi, Luciano Baresi

Publication date: 27 July 2020

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: http://hdl.handle.net/11311/1135498

zbMATH Keywords

formal verificationtimed automatabig datametric temporal logic

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Uses Software

• Kronos
• SPIN
• NuSMV
• Uppaal
• GitHub

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A tool for deciding the satisfiability of continuous-time metric temporal logic
• A survey of timed automata for the development of real-time systems
• Constraint LTL satisfiability checking without automata
• Model-checking in dense real-time
• A logical characterization of timed regular languages
• An automata-theoretic approach to constraint LTL
• A theory of timed automata
• Partial-order methods for the verification of concurrent systems. An approach to the state-explosion problem
• Scheduling with timed automata
• A decomposition theorem for partially ordered sets
• Model-checking Timed Temporal Logics
• Well-structured transition systems everywhere!

This page was built for publication: Using formal verification to evaluate the execution time of Spark applications