AVIACC
Analysis and Verification of Concurrent Critical Programs
FCOMP-01-012244-FEDER-020486 PTDC/EIA-CCO/117590 3 years (May 2012 to Apr 2015) | |
Summary: | The goal of the project is to extract models from concurrent programs and building an automatic framework for checking (temporal) properties using verification technologies, both static and run-time. |
Funding: | Global: 94KEUR, CISTER: 24.1KEUR |
Sponsors: | |
Partners: | |
Contact Person at CISTER: | Luis Miguel Pinho |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Journal Papers
Deciding Kleene Algebra Terms Equivalence in Coq CISTER-TR-141205
David Pereira, Nelma Moreira, Simão Patrício Melo de SousaJournal of Logical and Algebraic Methods in Programming (JLAMP), Elsevier. May 2015, Volume 84, Issue 3, pp 377-401.
David Pereira, Nelma Moreira, Simão Patrício Melo de SousaJournal of Logical and Algebraic Methods in Programming (JLAMP), Elsevier. May 2015, Volume 84, Issue 3, pp 377-401.
Logic-based schedulability analysis for compositional hard real-time embedded systems CISTER-TR-150411
André Pedro, David Pereira, Luis Miguel Pinho, Jorge Sousa PintoSIGBED Review (SIGBED Rev.), ACM. Feb 2015, Volume 12, Issue 1, pp 56-64.
André Pedro, David Pereira, Luis Miguel Pinho, Jorge Sousa PintoSIGBED Review (SIGBED Rev.), ACM. Feb 2015, Volume 12, Issue 1, pp 56-64.
Conference or Workshop Papers/Talks
WCET Measurement-based and Extreme Value Theory Characterisation of CUDA Kernels CISTER-TR-141009
Kostiantyn Berezovskyi, Luca Santinelli, Konstantinos Bletsas, Eduardo Tovar22nd International Conference on Real-Time Networks and Systems (RTNS 2014). 8 to 10, Oct, 2014. Versailles, France.
Kostiantyn Berezovskyi, Luca Santinelli, Konstantinos Bletsas, Eduardo Tovar22nd International Conference on Real-Time Networks and Systems (RTNS 2014). 8 to 10, Oct, 2014. Versailles, France.
Towards a Runtime Verification Framework for the Ada Programming Language CISTER-TR-140305
André Pedro, David Pereira, Luis Miguel Pinho, Jorge Sousa PintoLecture Notes in Computer Science, Reliable Software Technologies – Ada-Europe 2014 (LNCS), Springer International Publishing. 23 to 27, Aug, 2014, 8454, pp 58-73.
André Pedro, David Pereira, Luis Miguel Pinho, Jorge Sousa PintoLecture Notes in Computer Science, Reliable Software Technologies – Ada-Europe 2014 (LNCS), Springer International Publishing. 23 to 27, Aug, 2014, 8454, pp 58-73.
A Compositional Monitoring Framework for Hard Real-Time Systems CISTER-TR-140104
André Pedro, David Pereira, Luis Miguel Pinho, Jorge Sousa PintoNASA Formal Methods Symposium 2014 (NFM14), Springer International Publishing. 29, Apr, 2014, LNCS 8430, pp 16-30. Houston, TX, U.S.A..
André Pedro, David Pereira, Luis Miguel Pinho, Jorge Sousa PintoNASA Formal Methods Symposium 2014 (NFM14), Springer International Publishing. 29, Apr, 2014, LNCS 8430, pp 16-30. Houston, TX, U.S.A..
Logic-based Schedulability Analysis for Compositional Hard Real-Time Embedded Systems CISTER-TR-131201
André Pedro, David Pereira, Luis Miguel Pinho, Jorge Sousa Pinto6th International Workshop on Compositional Theory and Technology for Real-Time Embedded Systems (CRTS 2013). 3, Dec, 2013. Vancouver, Canada.Co-located within the IEEE Real-Time Systems Symposium (RTSS'13).
André Pedro, David Pereira, Luis Miguel Pinho, Jorge Sousa Pinto6th International Workshop on Compositional Theory and Technology for Real-Time Embedded Systems (CRTS 2013). 3, Dec, 2013. Vancouver, Canada.Co-located within the IEEE Real-Time Systems Symposium (RTSS'13).
Tasklettes – a Fine Grained Parallelism for Ada on Multicores CISTER-TR-130304
Stephen Michell, Brad Moore, Luis Miguel Pinho18th International Conference on Reliable Software Technologies (Ada-Europe 2013). 10 to 14, Jun, 2013, pp 17-34. Berlin, Germany.
Stephen Michell, Brad Moore, Luis Miguel Pinho18th International Conference on Reliable Software Technologies (Ada-Europe 2013). 10 to 14, Jun, 2013, pp 17-34. Berlin, Germany.
Parallelism in Ada: General Model and Ravenscar CISTER-TR-130405
Brad Moore, Stephen Michell, Luis Miguel Pinho16th International Real-Time Ada Workshop (IRTAW 2013), ACM New York. 17 to 19, Apr, 2013, 33, 2, pp 14-32. York, United Kingdom.
Brad Moore, Stephen Michell, Luis Miguel Pinho16th International Real-Time Ada Workshop (IRTAW 2013), ACM New York. 17 to 19, Apr, 2013, 33, 2, pp 14-32. York, United Kingdom.
Ada and Many-core Platforms CISTER-TR-130404
Luis Miguel Pinho, Stephen Michell, Brad Moore16th International Real-Time Ada Workshop (IRTAW 2013), ACM New York. 17 to 19, Apr, 2013, 33, 2, pp 40-48. York, United Kingdom.
Luis Miguel Pinho, Stephen Michell, Brad Moore16th International Real-Time Ada Workshop (IRTAW 2013), ACM New York. 17 to 19, Apr, 2013, 33, 2, pp 40-48. York, United Kingdom.
Conference or Workshop Posters/Demos
Towards Specification and Verification Frameworks for Concurrent Real-Time Systems CISTER-TR-130109
David Pereira, André Pedro, Luis Miguel Pinho, Jorge Sousa PintoPoster presented in High Integrity Language Technology ACM SIGAda’s Annual International Conference (HILT 2012). 2 to 6, Dec, 2012. Boston, U.S.A..
David Pereira, André Pedro, Luis Miguel Pinho, Jorge Sousa PintoPoster presented in High Integrity Language Technology ACM SIGAda’s Annual International Conference (HILT 2012). 2 to 6, Dec, 2012. Boston, U.S.A..