AVIACC

Analysis and Verification of Critical Concurrent Programs

Currently submitted

  • André de Matos Pedro, David Pereira, Luís Miguel Pinho, and Jorge Sousa Pinto. Monitoring for a decidable fragment of MTL-􏰃S. Submitted to Runtime Verification 2015.

  • Sabine Broda, Sílvia Cavadas, Miguel Ferreira, and Nelma Moreira. Synchronous Kleene algebra with derivatives. Submitted to an international conference.

  • Cezar Câmpeanu, Nelma Moreira, and Rogério Reis. Distinguishability operations on regular languages. Submitted for publication in Fundamenta Informaticae.

  • P. Soares, A. Ravara, and S. Melo de Sousa. Revisiting concurrent separation logic. Science of Computer Programming, 2014. Special issue on open problems in Concurrency Theory. Elsevier. Submitted in November 2014.

Publications in International Journals

Conditionally accepted for publication

  • Rovedy Aparecida Busquim e Silva, Nanci Naomi Arai, Luciana Akemi Burgareli, José Maria Parente de Oliveira, and Jorge Sousa Pinto. Formal verification with Frama-C: a case study in the space software domain. IEEE Transactions on Reliability, 2015. Conditionally accepted.

  • Mário Pereira and Simão Melo de Sousa. Complexity checking of ARM programs, by deduction -- extended and updated version. Science of Computer Programming, 2014. Selected papers of ACM SAC-SVT’14. Elsevier. Conditionally accepted in March 2015.

2015

  • V. Rodrigues, B. Akesson, M. Florido, S. Melo de Sousa, J. P. Pedroso, and P. Vasconcelos. Certifying execution time in multicores. Science of Computer Programming, 2014. Submitted in 2013 and accepted for publication in April 2014. To appear.

  • A. M. Pedro, D. Pereira, L. M. Pinho, and J. S. Pinto. Logic-based schedulability analysis for compositional hard real-time embedded systems. In SIGBED review 12(1):56–64. New York, NY, USA, 2015. ACM. link

  • Nelma Moreira, David Pereira, and Simão Melo de Sousa. Deciding Kleene algebra terms equivalence in Coq. Journal of Logical and Algebraic Methods in Programming, 84(3):377 – 401, 2015. link

Publications in Proceedings of Refereed International Events

2015

  • Pedro Soares, António Ravara, and Simão Melo de Sousa. Revisiting concurrent separation logic and operational semantics. In Masoud Daneshtalab, Marco Aldinucci, Ville Leppaenen, Johan Lilius, and Mats Brorsson, editors, 23rd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing, PDP 2015, Turku, Finland, March 4-6, 2015, pages 484–491. IEEE, 2015. link

  • Sabine Broda, António Machiavelo, Nelma Moreira, and Rogério Reis. Partial derivative automaton for regular expressions with shuffle. In Alexander Okhtin and Jeffrey Shallit, editors, Proceedings of Descriptional Complexity of Formal Systems, 17th International Workshop (DCFS 2015), 2014. To appear in Springer LNCS.

  • Eva Maia, Nelma Moreira, and Rogério Reis. Prefix and right-partial derivative automata. In Mariya Soskova and Victor Mitrana, editors, Proceedings of Computability in Europe (CiE 2015), 2015. To appear in Springer LNCS.

  • Nelma Moreira, Giovanni Pighizzini, and Rogério Reis. Optimal state reductions of automata with partially specified behaviors. In Giuseppe F. Italiano, Tiziana Margaria-Steffen, Jaroslav Pokorny, Jean-Jacques Quisquater, and Roger Wattenhofer, editors, SOFSEM 2015: Theory and Practice of Computer Science - 41st International Conference on Current Trends in Theory and Practice of Computer Science, Czech Republic, January 24-29, 2015. Proceedings, volume 8939 of Lecture Notes in Computer Science. Springer, 2015. link

2014

  • Mário Pereira and Simão Melo de Sousa. Complexity checking of ARM programs, by deduction. In Proceedings of the 2014 ACM SIGAPP Simposium on Applied Computing, Software Verification and Testing (ACM SAC-SVT'14). March 2014, Gyeongju, Korea. ACM Press. link

  • Eva Maia, Nelma Moreira, and Rogério Reis. Partial derivative and position bisimilarity automata. In Markus Holzer and Martin Kutrib, editors, Implementation and Application of Automata - 19th International Conference, CIAA 2014, Giessen, Germany, July 30 - August 2, 2014. Proceedings, volume 8587 of Lecture Notes in Computer Science. Springer, 2014. link

  • Cezar Câmpeanu, Nelma Moreira, and Rogério Reis. The distinguishability operation on regular languages. In Suna Bensch, Rudolf Freund, and Friedrich Otto, editors, Sixth Workshop on Non-Classical Models for Automata and Applications - NCMA 2014, Kassel, Germany, July 28-29, 2014. Proceedings, volume 304 of books@ocg.at. Oesterreichische Computer Gesellschaft, 2014. link

  • Sabine Broda, António Machiavelo, Nelma Moreira, and Rogério Reis. "On the Equivalence of Automata for KAT-expressions". In A. Beckmann, E. Csuhaj-Varjú, K. Meer (eds.): Computability in Europe (CIE 2014), LNCS 8493, Springer 2014. link

  • A. de Matos Pedro, D. Pereira, L. M. Pinho, and J. S. Pinto. Towards a Runtime Verification Framework for the Ada Programming Language. In Proceedings of the 19th International Conference on Reliable Software Technologies (RST-AE’14), Lecture Notes in Computer Science, Berlin, Heidelberg, 2014. Springer-Verlag. link

  • A. de Matos Pedro, D. Pereira, L. M. Pinho, and J. S. Pinto. A Compositional Monitoring Framework for Hard Real-Time Systems. In Proceedings of the Sixth NASA Formal Methods Symposium (NFM 2014), Lecture Notes in Computer Science, Berlin, Heidelberg, 2014. Springer-Verlag. link

  • N. Carvalho, C. da Silva Sousa, J. S. Pinto, and A. Tomb. Formal Verification of kLIBC with the WP Frama-C plug-in. In Proceedings of the Sixth NASA Formal Methods Symposium (NFM 2014), Lecture Notes in Computer Science, Berlin, Heidelberg, 2014. Springer-Verlag. link

  • C. B. Lourenço, M. J. Frade, and J. S. Pinto. A Bounded Model Checker for SPARK Programs (tool paper). In Proceedings of Automated Technology for Verification and Analysis - 12th International Symposium (ATVA 2014), volume 8837 of Lecture Notes in Computer Science, pages 24–30, Berlin, Heidelberg, 2014. Springer-Verlag. link

2013

  • V. Rodrigues, B. Akesson, S. M. de Sousa, M. Florido: A Declarative Compositional Timing Analysis for Multicores Using the Latency-Rate Abstraction. PADL 2013: 43-59. link

  • S. Broda, A. Machiavelo, N. Moreira, R. Reis, "On the Average Size of Glushkov and Equation Automata for KAT Expressions", in 19th International Symposium on Fundamentals of Computation Theory, number 8070 in LNCS, pages 72-83. Springer-Verlag, 2013. link

  • I. Abal and J. S. Pinto. 2013. Towards a mostly-automated prover for bit-vector arithmetic. In Proceedings of the International C* Conference on Computer Science and Software Engineering (C3S2E '13). ACM, New York, NY, USA, 132-133. link

  • R. A. B. e Silva, N. N. Arai, L. A. Burgareli, J. M. P. Oliveira, J. S. Pinto. Using Abstract Interpretation to Produce Dependable Aerospace Control Software. Presented at the Sixth Latin-American Symposium on Dependable Computing (LADC'2013), industrial track. link

  • D. da Cruz, P. R. Henriques, and J. S. Pinto. Interactive Verification of Safety-Critical Software. In proceedings of the 37th Annual International Computer Software & Applications Conference (COMPSAC 2013), IEEE. link

2012

  • R. Almeida, S. Broda, N. Moreira, "Deciding KAT and Hoare Logic with Derivatives", Proceedings of the Third International Symposium on Games, Automata, Logics and Formal Verification (GandALF 2012), Electronic Proceedings in Theoretical Computer Science, pp. 127-140, 2012. link

  • D. Pereira, A. Pedro, L. M. Pinho and J. S. Pinto, “Towards specification and verification frameworks for concurrent real-time systems”, Poster presented at the ACM SIGAda High Integrity Language Technology 2012 conference in Boston, MA, December 2-6. link

Communications and Publications in National Events

  • Nuno Laranjo, Rogério Pontes, , and Maria João Frade. HSMTLib – interacting with SMT solvers in haskell. 2014. Poster presented at INForum’14 — Simpósio de Informática. link

  • V. C. Miraldo, M. J. Frade, C. Lourenço, and J. S. Pinto. Experimenting with predicate abstraction. In B. S. Santos and J. Cachopo, editors, Proceedings of INForum’13 — Simpósio de Informática (SOFTPT track). Universidade de Évora, 2013. link

  • V. C. Miraldo, M. J. Frade, C. Lourenço, and J. S. Pinto. SPARK-BMC: Checking spark code for bugs (Comunicação). Simpósio de Informática (SETR track). Universidade de Évora, 2013. link

  • Mário Pereira, Jean-Christophe Filliâtre, and Simão Melo de Sousa. ARMY: a deductive verification platform for ARM programs using Why3. In INForum 2012, September 2012. link

Reports

  • Cláudio Belo Lourenço, Maria João Frade, and Jorge Sousa Pinto. A single- assignment translation for while annotated programs. Technical report, HASLab & Universidade do Minho, 2014. link

  • Victor Cacciari Miraldo, Experimenting with Predicate Abstraction. Technical Report. link

  • Victor Cacciari Miraldo, SABS : A Spark ABStraction Tutorial. Technical Report. link

  • Sabine Broda, Sílvia Cavadas, and Nelma Moreira. Derivative based methods for deciding SKA and SKAT. Technical Report DCC-2014-10, DCC-FC, Universidade do Porto, 2014. link

  • Sabine Broda, Sílvia Cavadas, and Nelma Moreira. Kleene Algebra Completeness. Technical Report DCC-2014-07, DCC-FC & CMUP, Universidade do Porto, April 2014. link

  • Sabine Broda, António Machiavelo, Nelma Moreira, and Rogério Reis. Automata for KAT Expressions. Technical Report DCC-2014-01, DCC-FC, Universidade do Porto, January 2014. link

  • Nelma Moreira, David Pereira, and Simão Melo de Sousa. On the Mechanisation of Rely-Guarantee in Coq. Technical Report DCC-2013-01, DCC-FC, Universidade do Porto, January 2013. link

  • Vítor Rodrigues. Compositional timing analysis for multicores using the latency-rate abstraction. Technical report, DCC-FC, Universidade do Porto, 2012. link

Theses

Forthcoming

  • André de Matos Pedro. Dynamic contracts for Verification and Enforcement of Real-time Systems Properties. PhD thesis, MAPi PhD program, Universidade do Minho, 2016. Forthcoming.

  • Cláudio Belo Lourenço. Software Verification and Defect Analysis. PhD thesis, MAPi PhD program, Universidade do Minho, 2017. Forthcoming.

Defended

  • Rovedy Aparecida Busquim e Silva. Uma Abordagem de Engenharia Reversa para Extracção do Projeto de Sistemas de Software Crítico Embarcado. PhD thesis, Instituto Tecnológico de Aeronáutica, 2013. link

  • Vitor Rodrigues. Semantics-based Program Verification: An Abstract Interpretation Approach. PhD Thesis. MAPi PhD program, LIACC/DCC/FCUP - University of Porto. May 2013. link

  • David Pereira. Towards Certified Program Logics for the Verification of Imperative Programs. PhD Thesis. MAPi PhD program, LIACC/DCC/FCUP - University of Porto. April 2013. link

  • Claúdio Belo Lourenço, A SPARK Model Checker for SPARK programas. MSc thesis. Universidade do Minho, 2013. link

r15 - 04 Jan 2016 - 18:00:54 - JorgeSousaPinto
This site is powered by the TWiki collaboration platform Copyright © by the contributing authors. Ideas, requests, problems? Send feedback.
Syndicate this site RSSATOM