In a brief comparison of software model checking with deductive verification techniques for the purpose of verifying concurrent software, we stress the following:
The state of the art of software model checking techniques is substantially more advanced than deductive techniques. More interesting and complex properties can be automatically proved than with deductive methods. Consequently these methods are much more used in industry than deductive methods.
The above does not mean that deductive methods are doomed to be abandoned: on one hand the soundness and completeness of these methods (with no false errors), as well as the expressiveness of the logical languages used and the general flexibility of their application make them highly desirable (especially in the critical context); on the other hand it is expected that, as was previously the case for sequential code, automation levels will increase and render such methods more usable.
The current project has the double purpose of advancing the state of the art and providing results that can be brought to practice in the very short term by our industrial partners. Since software model checking techniques are currently much more advanced and usable in practice than deductive methods, one task of the project will be dedicated to producing a practical verification platform suited to specific needs and programming languages. On the other hand, the deduction-based approach to verification of concurrent software has become an exciting area, in which the team wants to contribute with fundamental research.
Our approach will be guided by three simples principles, as follows:
It will be incremental, starting from languages with restricted data structures and models for concurrency. This is particularly adequate for critical software, since in this area the programming languages that are used are often subject to restricted profiles that forbid less predictable behaviour.
It will combine path sensitive and path insensitive techniques, and exploit their interaction. It is our firm belief that the key to successful automatic verification lies in this combined approach.
All the methods and tools produced will be validated through real-life use cases, provided and carried out by team members who work directly in the development of embedded critical software.
We now detail our plan and the reasons why we think these three principles will lead us to successful solutions.
I.
Since C and Ada are the languages of choice in the development of embedded critical systems, we will start by addressing the
verification of concurrent programs of subsets of both languages. In
the case of Ada, the choice goes naturally to the RavenSPARK language, which has the enormous advantage of being a commercially successful product, widely used in industry, and having ideal characteristics for
our purposes: a restricted model of concurrency; restricted data structures (no aliasing is possible); an annotation language comprising assertional and dataflow contracts; and the availability of a toolset for checking both dataflow and assertions. Furthermore the team possesses experience in the verification of sequential SPARK code.
The presence of dataflow annotations, complemented by a model of concurrency that forbids the dynamic creation of threads, can be taken into account to calculate predicate abstractions of concurrent programs, since the amount of interference between threads is naturally limited by the dataflow restrictions, which can be taken for granted since they can be effectively checked by the SPARK toolset. Also, rely and guarantee conditions are intrinsically related to
dataflow annotations of individual threads of a program. It will be interesting for instance to see if such conditions can be automatically inferred from the compulsory dataflow annotations that must be present in every valid RavenSPARK program.
II.
Approaches to program verification that combine different techniques are seen as promising, even if it may be difficult for a team to
acquire the required know-how. We intend precisely to take advantage of the fact that know-how is in place, as a result of a process
carried out over the past 5 years in a number of projects, collaborations, and doctoral theses.
Predicate abstraction, which is a fundamental component of any software model checking system, is typically implemented with the help of a weakest precondition algorithm -- a deductive technique. In this project we will be in a position of deep understanding of the
deductive aspects of verification, which may allow us to produce predicate abstraction algorithms tailored to our needs. Moreover,
since the study of predicate abstractions for concurrent programs is a practically untouched field, it may well be the case that the rely-guarantee principles and verification conditions algorithms can
be used fruitfully for predicate abstraction (some published work
hints at this).
Finally, it is our conviction that a mixture of software model
checking and deductive verification can be in itself a very powerful verification method. Rely-guarantee reasoning is based on two separate aspects: "intra-thread" verification conditions for each thread
(taking as assumptions rely and guarantee conditions of all the
threads in the program), and "inter-thread" verification conditions,
to assert (compositionally) that if all threads satisfy a given
property then the ensemble does so as well. We will investigate the possibility of each of these aspects being verified by different
methods; we will for instance use a SMC to check intra-thread properties and rely-guarantee reasoning for the compositional aspect. This may still result in an acceptable level of automation in the
proofs. In the other direction we will also investigate the use of predicate abstraction itself as a tool for deductive verification at
the inter-thread level, since rely-guarantee VCs may be easier to establish for over-approximated code.
III.
This project stems from an ongoing collaboration between academics and practitioners. The team brings together
Specialists in verification from CCTC and CMAT, Univ Minho, and LIACC, Univ Porto, who will work on the theoretical aspects of all the main tasks of the project: predicate abstraction (CCTC and LIACC, task 1); properties of models (LIACC, task 2); and deductive techniques (CMAT, CCTC, and LIACC, task 3).
Researchers who are expert in embedded, safety-critical, and real-time concurrent programming, from CISTER, IPP, will work on the development of the SMC platform (task 2), provide use cases, and carry on an evaluation of the tools and methods obtained as outcomes of the project (task 4).
Main Results
The main results of the project will include (for at least one of the programming languages of interest in the safety-critical context)
a novel predicate abstraction algorithm and the corresponding implementation
a SMC toolkit for concurrent applications
a prototype generic SMC toolkit (multi-language, multi-checker)
a VCGen for rely-guarantee conditions
a general method for verification of concurrent programs combining both path-sensitive and path-insensitive techniques.
Main novelties include (i) taking advantage of specific aspects of relatively simple programming languages used in safety-critical development, and (ii) combining techniques that have not to this point been combined. Both aspects will allow us to produce tools that can be used with realistic code.
The formal verification of software is increasingly important in software engineering, particularly in the context of critical applications, which is regulated by norms that advise or enforce the use of formal or semi-formal validation techniques. Academic researchers are being led to collaborate with industry in the development of methods and tools that allow practitioners to incorporate formal verification in their validation process.
This project stems from an ongoing collaboration between three academic groups and software engineers working for companies that work precisely in safety-sensitive domains, subject to norms such as mentioned above.
After enormous developments in the verification of sequential software, industry is now able to employ formal verification
techniques in their projects, either based on model checking, abstract interpretation, or logical proofs. Unfortunately, safety-critical applications are usually inherently concurrent, which means that these are often of limited utility. Moreover, there is a mismatach between the programming languages that are receiving more attention from the research community and those that are used in practice in the safety-critical domain. Ada for instance, has paradoxically fallen out
of fashion as a general purpose programming language, but is more and more used in the safety-critical domain (a fact of which academics are seldom aware). The languages that will be object of our study will include at least a subset of C and the RavenSPARK high integrity language, both widely used by practitioners in the critical domain.
The scope of the present project is the verification of properties of
shared memory concurrent programs, both advancing the state of the art at the theoretical level and producing tools that can be used
by companies developing critical applications. Our approach will focus simultaneously on two techniques: software model checking
and deductive reasoning. Crucially, advances in each technique have historically fed back into the other technique, and we believe such a mixed approach (which is made possible by the know-how accumulated by the team over the last five years) can be fruitful.
Goals
The goals of the project are (labelled [T]heoretical or [P]ractical):
1. [T] To investigate abstraction techniques that can be used to tame the state explosion problem inherent to any programming language with a realistic set of types. For this we will build on recent work, in
particular on predicate abstraction. We hope to be able to propose enhancements to the published abstraction mechanisms, in particular stemming from the work on deductive compositional verification methods that will take place in parallel (see below).
It is not our goal to investigate model checking algorithms; our
interest is in the extraction of approximated models from the source code and in checking properties of these models using a standard model checker. This allows us to automatically take benefit from the wealth
of work accumulated on taming other sources of state explosion like control flow.
2. [P] (building on 1) To produce software model checking tools for
our object languages. The approach to be followed can be summarized as follows: we will perform syntactical analysis of the source code, and apply abstraction techniques to obtain the control flow graph of an approximated version of the initial program. From this we will produce
a Labelled Transitions (LT) model. The tool will also translate properties (expressed as comments
in the source code) to properties expressed in the logic of the model checker, that
can be used to query it.
3. [P] (building on 2) To investigate the possibility of producing a common language for representing LT systems and properties of these systems. The idea would be that these models and properties can then be exported to more than one model checking tool. It may well be the case that some properties can be checked with one model checker, while another checker may be able to check other properties. In this generic approach we take inspiration from tools for deductive verification of sequential programs, like Why and Boogie.
4. [T,P] To propose a verification conditions generator (VCGen) for a (concurrent) subset of one of our object languages, based on rely-guarantee principles. The subset will be sufficiently simple to allow us to focus on the generation of verification conditions, and to put together a complete verification platform, consisting of the VCGen and a choice of SMT solvers to discharge the VCs.
5. [T] (building on 4) To study extensions of the rely-guarantee
system to accommodate progressively richer features of the programming language, including heap-based dynamic structures. We will consider in particular combinations with formalisms like separation logic and
typed memory.
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
TWiki's Research/Aviacc webThe Research/Aviacc web of TWiki. TWiki is a Web-Based Collaboration Platform for the Enterprise.http://wiki.di.uminho.pt/twiki/bin/view/Research/AviaccCopyright 2020 by contributing authors2016-01-04T18:00:54ZPublicationshttp://wiki.di.uminho.pt/twiki/bin/view/Research/Aviacc/Publications2016-01-04T18:00:54ZCurrently submitted André de Matos Pedro, David Pereira, Luís Miguel Pinho, and Jorge Sousa Pinto. Monitoring for a decidable fragment of MTL #1113091;S. Submitted ... (last changed by JorgeSousaPinto)JorgeSousaPintoToolshttp://wiki.di.uminho.pt/twiki/bin/view/Research/Aviacc/Tools2015-05-20T09:17:14ZSoftware Tools and Packages HSMTlib A Haskell library for easy interaction with multiple SMT solvers. Available through Hackage. SPARK parser A parser library for ... (last changed by JorgeSousaPinto)JorgeSousaPintoWebSideBarhttp://wiki.di.uminho.pt/twiki/bin/view/Research/Aviacc/WebSideBar2015-05-19T13:20:29ZOverview Home Project Proposal Team Research Team Job Opportunities Results Publications Tools Events First Project Meeeting ... (last changed by JorgeSousaPinto)JorgeSousaPinto2ndWorkshophttp://wiki.di.uminho.pt/twiki/bin/view/Research/Aviacc/2ndWorkshop2015-05-19T13:19:43ZAVIACC Second Meeting and Workshop Date September 16, 2013, 10:00 Place DCC FCUP, videoconference room Schedule 10h00 12h30: Scientific talks and discussion 14h30 ... (last changed by JorgeSousaPinto)JorgeSousaPinto1stWorkshophttp://wiki.di.uminho.pt/twiki/bin/view/Research/Aviacc/1stWorkshop2015-05-19T13:19:33ZAVIACC First Project Meeting Date December 18, 2012, 10:00 Place DCC FCUP, videoconference room Schedule 10h00 11h30: Scientific talks and discussion 11h30 ... (last changed by JorgeSousaPinto)JorgeSousaPintoJobshttp://wiki.di.uminho.pt/twiki/bin/view/Research/Aviacc/Jobs2014-04-23T11:17:00ZBI Grant Announcements of a Bounded Model Checker for SPARK closed Abstraction for Critical Programs closed and tools for the analysis and verification ... (last changed by JorgeSousaPinto)JorgeSousaPintoTeamhttp://wiki.di.uminho.pt/twiki/bin/view/Research/Aviacc/Team2014-04-23T11:07:22ZSenior Researchers Sabine Broda FCUP Daniela da Cruz UM Maria João Frade UM Nelma Moreira FCUP David Pereira IPP Luís Miguel ... (last changed by JorgeSousaPinto)JorgeSousaPintoWebHomehttp://wiki.di.uminho.pt/twiki/bin/view/Research/Aviacc/WebHome2014-04-22T15:30:07ZAnalysis and Verification of Critical Concurrent Programs The scope of the present project is the verification of properties of safety critical software. Our approach ... (last changed by JorgeSousaPinto)JorgeSousaPintoDescriptionhttp://wiki.di.uminho.pt/twiki/bin/view/Research/Aviacc/Description2013-02-20T11:22:26ZMotivation In a brief comparison of software model checking with deductive verification techniques for the purpose of verifying concurrent software, we stress the ... (last changed by JorgeSousaPinto)JorgeSousaPintoProjectSummaryhttp://wiki.di.uminho.pt/twiki/bin/view/Research/Aviacc/ProjectSummary2013-02-18T18:51:40ZProject Summary The formal verification of software is increasingly important in software engineering, particularly in the context of critical applications, which ... (last changed by JorgeSousaPinto)JorgeSousaPintoWebPreferenceshttp://wiki.di.uminho.pt/twiki/bin/view/Research/Aviacc/WebPreferences2013-02-18T17:30:17ZResearch/Aviacc Web Preferences The following settings are web preferences of the Research/Aviacc web. These preferences overwrite the site level preferences ... (last changed by JorgeSousaPinto)JorgeSousaPintoNewshttp://wiki.di.uminho.pt/twiki/bin/view/Research/Aviacc/News2013-01-10T14:59:52ZThe first project meeting took place on December 18 2012, at FCUP. (last changed by JorgeSousaPinto)JorgeSousaPintoWebStatisticshttp://wiki.di.uminho.pt/twiki/bin/view/Research/Aviacc/WebStatistics2012-12-20T06:57:54ZStatistics for Research/Aviacc Web Month: Topic views: Topic saves: File uploads: Most popular topic views: Top contributors for topic ... (last changed by TWikiGuest)TWikiGuestWebTopicListhttp://wiki.di.uminho.pt/twiki/bin/view/Research/Aviacc/WebTopicList2006-11-15T19:43:52Z (last changed by TWikiContributor)TWikiContributorWebSearchAdvancedhttp://wiki.di.uminho.pt/twiki/bin/view/Research/Aviacc/WebSearchAdvanced2006-11-15T19:43:52Z (last changed by TWikiContributor)TWikiContributorWebTopicCreatorhttp://wiki.di.uminho.pt/twiki/bin/view/Research/Aviacc/WebTopicCreator2006-11-15T19:43:52Z (last changed by TWikiContributor)TWikiContributor
Currently submitted André de Matos Pedro, David Pereira, Luís Miguel Pinho, and Jorge Sousa Pinto. Monitoring for a decidable fragment of MTL #1113091;S. Submitted ...
Software Tools and Packages HSMTlib A Haskell library for easy interaction with multiple SMT solvers. Available through Hackage. SPARK parser A parser library for ...
AVIACC Second Meeting and Workshop Date September 16, 2013, 10:00 Place DCC FCUP, videoconference room Schedule 10h00 12h30: Scientific talks and discussion 14h30 ...
AVIACC First Project Meeting Date December 18, 2012, 10:00 Place DCC FCUP, videoconference room Schedule 10h00 11h30: Scientific talks and discussion 11h30 ...
BI Grant Announcements of a Bounded Model Checker for SPARK closed Abstraction for Critical Programs closed and tools for the analysis and verification ...
Analysis and Verification of Critical Concurrent Programs The scope of the present project is the verification of properties of safety critical software. Our approach ...
Motivation In a brief comparison of software model checking with deductive verification techniques for the purpose of verifying concurrent software, we stress the ...
Project Summary The formal verification of software is increasingly important in software engineering, particularly in the context of critical applications, which ...
Research/Aviacc Web Preferences The following settings are web preferences of the Research/Aviacc web. These preferences overwrite the site level preferences ...
Analysis and Verification of Critical Concurrent Programs
The scope of the present project is the verification of properties of safety-critical software. Our approach will focus simultaneously on two techniques: software model checking and deductive reasoning, both advancing the state of the art at the theoretical level and producing tools that can be used by companies developing critical applications. We are particularly interested in interactions between both approaches, which have historically fed back into each other.
One particular topic that will be investigated is the formal verification of shared memory concurrent programs, elucidating the feasibility of their use in the safety-critical context.
(read more)
Project info
Este trabalho é financiado por Fundos FEDER através do Programa Operacional Fatores de Competitividade - COMPETE e por Fundos Nacionais através da FCT - Fundação para a Ciência e a Tecnologia no âmbito do projeto FCOMP-01-0124-FEDER-020486
This work is funded by ERDF - European Regional Development Fund through the COMPETE Programme (operational programme for competitiveness) and by National Funds through the FCT - Fundação para a Ciência e a Tecnologia (Portuguese Foundation for Science and Technology) within project FCOMP-01-0124-FEDER-020486
Supported by
under contract PTDC/EIA-CCO/108995/2008 (94 KEuro)
AVIACC First Project Meeting Date December 18, 2012, 10:00 Place DCC FCUP, videoconference room Schedule 10h00 11h30: Scientific talks and discussion 11h30 ...
AVIACC Second Meeting and Workshop Date September 16, 2013, 10:00 Place DCC FCUP, videoconference room Schedule 10h00 12h30: Scientific talks and discussion 14h30 ...
Motivation In a brief comparison of software model checking with deductive verification techniques for the purpose of verifying concurrent software, we stress the ...
BI Grant Announcements of a Bounded Model Checker for SPARK closed Abstraction for Critical Programs closed and tools for the analysis and verification ...
Project Summary The formal verification of software is increasingly important in software engineering, particularly in the context of critical applications, which ...
Currently submitted André de Matos Pedro, David Pereira, Luís Miguel Pinho, and Jorge Sousa Pinto. Monitoring for a decidable fragment of MTL #1113091;S. Submitted ...
Software Tools and Packages HSMTlib A Haskell library for easy interaction with multiple SMT solvers. Available through Hackage. SPARK parser A parser library for ...
Analysis and Verification of Critical Concurrent Programs The scope of the present project is the verification of properties of safety critical software. Our approach ...
Research/Aviacc Web Preferences The following settings are web preferences of the Research/Aviacc web. These preferences overwrite the site level preferences ...
This is a subscription service to be automatically notified by e-mail when topics change in this Research/Aviacc web. This is a convenient service, so you do not have to come back and check all the time if something has changed. To subscribe, please add a bullet with your WikiName in alphabetical order to this list:
Each TWiki web has an automatic e-mail notification service that sends you an e-mail with links to all of the topics modified since the last alert.
Users subscribe to email notifications using their WikiName or an alternative email address, and can specify the webs/topics they wish to track using one of these bullet list formats:
three spaces * [ webname . ] wikiName - SMTP mail address three spaces * [ webName . ] wikiName three spaces * SMTP mail address three spaces * SMTP mail address : topics three spaces * [ webname . ] wikiName : topics
In the above examples, topics is a space-separated list of topic names. The user may further customize the specific content they will receive using the following formats:
Specify topics without a Web. prefix
Topics must exist in this web.
Topics may be specified using * wildcards
Each topic may optionally be preceded by a '+' or '-' sign. The '+' sign means "subscribe to this topic" (the same as not putting anything). The '-' sign means "unsubscribe" or "don't send notifications regarding this topic". This allows users to elect to filter out certain topics (and their children, to an arbitrary depth). Topic filters ('-') take precedence over topic includes ('+').
Each topic may optionally be followed by an integer in parentheses, indicating the depth of the tree of children below that topic. Changes in all these children will be detected and reported along with changes to the topic itself. Note This uses the TWiki "Topic parent" feature.
Each topic may optionally be immediately followed by an exclamation mark ! or a question mark ? with no intervening spaces, indicating that the topic (and children if there is a tree depth specifier as well) should be mailed out as complete topics instead of change summaries. ! causes the topic to be mailed every time even if there have been no changes, ? will mail the topic only if there have been changes to it. This only makes sense for subscriptions.
For example:
Subscribe Daisy to all changes to topics in this web.
* daisy.cutter@flowers.com
Subscribe Daisy to all changes in all webs that start with Web.
* daisy.cutter@flowers.com: Web*
Subscribe Daisy to changes to topics starting with Petal, and their immediate children, WeedKillers and children to a depth of 3, and all topics that match start with Pretty and end with Flowers e.g. PrettyPinkFlowers
Subscribe Daisy to the full content of NewsLetter whenever it has changed
* daisy@flowers.com: TWiki.NewsLetter?
Subscribe buttercup to NewsLetter and its immediate children, even if it hasn't changed.
* buttercup@flowers.com: TWiki.NewsLetter! (1)
Subscribe GardenGroup (which includes Petunia) to all changed topics under AllnewsLetters to a depth of 3. Then unsubscribe Petunia from the ManureNewsLetter, which she would normally get as a member of GardenGroup? :
A user may be listed many times in the WebNotify topic. Where a user has several lines in WebNotify that all match the same topic, they will only be notified about changes that topic once (though they will still receive individual mails for news topics).
If a TWiki group is listed for notification, the group will be recursively expanded to the e-mail addresses of all members.
Tip: List names in alphabetical order to make it easier to find the names.
Note for System Administrators: Notification is supported by an add-on to the TWiki kernel called the MailerContrib. See the MailerContrib topic for details of how to set up this service.
Note: If you prefer a news feed, point your reader to WebRss (for RSS 1.0 feeds) or WebAtom (for ATOM 1.0 feeds). Learn more at WebRssBase and WebAtomBase, respectively.
Related topics:WebChangesAlert, TWikiUsers, TWikiRegistration
These settings override the defaults for this web only. See full list of defaults with explanation. Many of the settings below are commented out. Remove the # sign to enable a local customisation.
Web-specific background color: (Pick a lighter one of the StandardColors).
Set WEBBGCOLOR = #D0D0D0
Note: This setting is automatically configured when you create a web
Image, URL and alternate tooltip text of web's logo. Note: Don't add your own local logos to the TWikiLogos topic; create your own logos topic instead.
List this web in the SiteMap. If you want the web listed, then set SITEMAPLIST to on, do not set NOSEARCHALL, and add the "what" and "use to..." description for the site map. Use links that include the name of the web, i.e. Research/Aviacc.Topic links. Note: Unlike other variables, the setting of SITEMAPLIST is not inherited from parent webs. It has to be set in every web that is to be listed in the SiteMap
Set SITEMAPLIST = on
Set SITEMAPWHAT = Projeto AVIACC
Set SITEMAPUSETO = Analysis and Verification of Critical Concurrent Programs
Note: Above settings are automatically configured when you create a web
Exclude web from a web="all" search: (Set to on for hidden webs).
Set NOSEARCHALL =
Note: This setting is automatically configured when you create a web
Prevent automatic linking of WikiWords and acronyms (if set to on); link WikiWords (if empty); can be overwritten by web preferences:
#Set NOAUTOLINK =
Note: You can still use the [[...][...]] syntax to link topics if you disabled WikiWord linking. The <noautolink> ... </noautolink> syntax can be used to prevents links within a block of text.
Default template for new topics for this web:
WebTopicEditTemplate? : Default template for new topics in this web. (Site-level is used if topic does not exist)
Comma separated list of forms that can be attached to topics in this web. See TWikiForms for more information.
Set WEBFORMS =
Users or groups who are not / are allowed to view / change / rename topics in the Research/Aviacc web: (See TWikiAccessControl). Remove the # to enable any of these settings. Remember that an empty setting is a valid setting; setting DENYWEBVIEW to nothing means that anyone can view the web.
Preferences are used as TWikiVariables by enclosing the name in percent signs. Example:
When you write variable %WEBBGCOLOR% , it gets expanded to #D0D0D0
The sequential order of the preference settings is significant. Define preferences that use other preferences first, i.e. set WEBCOPYRIGHT before WIKIWEBMASTER since %WEBCOPYRIGHT% uses the %WIKIWEBMASTER% variable.
You can introduce your own preferences variables and use them in your topics and templates.
TWiki search results for \.*
http://wiki.di.uminho.pt/twiki/bin/view/Research/Aviacc
The Research/Aviacc web of TWiki. TWiki is a Web-Based Collaboration Platform for the Enterprise.en-usCopyright 2020 by contributing authorsTWiki Administrator [webmaster@di.uminho.pt]The contributing authors of TWikiTWikiDIUM.Research/Aviacc
http://wiki.di.uminho.pt/twiki/bin/view/Research/Aviacc
/twiki/pub/Main/LocalLogos/um_eengP.jpgPublications
http://wiki.di.uminho.pt/twiki/bin/view/Research/Aviacc/Publications
Currently submitted André de Matos Pedro, David Pereira, Luís Miguel Pinho, and Jorge Sousa Pinto. Monitoring for a decidable fragment of MTL #1113091;S. Submitted ... (last changed by JorgeSousaPinto)2016-01-04T18:00:54ZJorgeSousaPintoTools
http://wiki.di.uminho.pt/twiki/bin/view/Research/Aviacc/Tools
Software Tools and Packages HSMTlib A Haskell library for easy interaction with multiple SMT solvers. Available through Hackage. SPARK parser A parser library for ... (last changed by JorgeSousaPinto)2015-05-20T09:17:14ZJorgeSousaPintoWebSideBar
http://wiki.di.uminho.pt/twiki/bin/view/Research/Aviacc/WebSideBar
Overview Home Project Proposal Team Research Team Job Opportunities Results Publications Tools Events First Project Meeeting ... (last changed by JorgeSousaPinto)2015-05-19T13:20:29ZJorgeSousaPinto2ndWorkshop
http://wiki.di.uminho.pt/twiki/bin/view/Research/Aviacc/2ndWorkshop
AVIACC Second Meeting and Workshop Date September 16, 2013, 10:00 Place DCC FCUP, videoconference room Schedule 10h00 12h30: Scientific talks and discussion 14h30 ... (last changed by JorgeSousaPinto)2015-05-19T13:19:43ZJorgeSousaPinto1stWorkshop
http://wiki.di.uminho.pt/twiki/bin/view/Research/Aviacc/1stWorkshop
AVIACC First Project Meeting Date December 18, 2012, 10:00 Place DCC FCUP, videoconference room Schedule 10h00 11h30: Scientific talks and discussion 11h30 ... (last changed by JorgeSousaPinto)2015-05-19T13:19:33ZJorgeSousaPintoJobs
http://wiki.di.uminho.pt/twiki/bin/view/Research/Aviacc/Jobs
BI Grant Announcements of a Bounded Model Checker for SPARK closed Abstraction for Critical Programs closed and tools for the analysis and verification ... (last changed by JorgeSousaPinto)2014-04-23T11:17:00ZJorgeSousaPintoTeam
http://wiki.di.uminho.pt/twiki/bin/view/Research/Aviacc/Team
Senior Researchers Sabine Broda FCUP Daniela da Cruz UM Maria João Frade UM Nelma Moreira FCUP David Pereira IPP Luís Miguel ... (last changed by JorgeSousaPinto)2014-04-23T11:07:22ZJorgeSousaPintoWebHome
http://wiki.di.uminho.pt/twiki/bin/view/Research/Aviacc/WebHome
Analysis and Verification of Critical Concurrent Programs The scope of the present project is the verification of properties of safety critical software. Our approach ... (last changed by JorgeSousaPinto)2014-04-22T15:30:07ZJorgeSousaPintoDescription
http://wiki.di.uminho.pt/twiki/bin/view/Research/Aviacc/Description
Motivation In a brief comparison of software model checking with deductive verification techniques for the purpose of verifying concurrent software, we stress the ... (last changed by JorgeSousaPinto)2013-02-20T11:22:26ZJorgeSousaPintoProjectSummary
http://wiki.di.uminho.pt/twiki/bin/view/Research/Aviacc/ProjectSummary
Project Summary The formal verification of software is increasingly important in software engineering, particularly in the context of critical applications, which ... (last changed by JorgeSousaPinto)2013-02-18T18:51:40ZJorgeSousaPintoWebPreferences
http://wiki.di.uminho.pt/twiki/bin/view/Research/Aviacc/WebPreferences
Research/Aviacc Web Preferences The following settings are web preferences of the Research/Aviacc web. These preferences overwrite the site level preferences ... (last changed by JorgeSousaPinto)2013-02-18T17:30:17ZJorgeSousaPintoNews
http://wiki.di.uminho.pt/twiki/bin/view/Research/Aviacc/News
The first project meeting took place on December 18 2012, at FCUP. (last changed by JorgeSousaPinto)2013-01-10T14:59:52ZJorgeSousaPintoWebChanges
http://wiki.di.uminho.pt/twiki/bin/view/Research/Aviacc/WebChanges
(last changed by TWikiContributor)2006-11-15T19:43:52ZTWikiContributorWebIndex
http://wiki.di.uminho.pt/twiki/bin/view/Research/Aviacc/WebIndex
(last changed by TWikiContributor)2006-11-15T19:43:52ZTWikiContributorWebSearch
http://wiki.di.uminho.pt/twiki/bin/view/Research/Aviacc/WebSearch
(last changed by TWikiContributor)2006-11-15T19:43:52ZTWikiContributorWebSearchAdvanced
http://wiki.di.uminho.pt/twiki/bin/view/Research/Aviacc/WebSearchAdvanced
(last changed by TWikiContributor)2006-11-15T19:43:52ZTWikiContributor
In a brief comparison of software model checking with deductive verification techniques for the purpose of verifying concurrent software, we stress the following:
The state of the art of software model checking techniques is substantially more advanced than deductive techniques. More interesting and complex properties can be automatically proved than with deductive methods. Consequently these methods are much more used in industry than deductive methods.
The above does not mean that deductive methods are doomed to be abandoned: on one hand the soundness and completeness of these methods (with no false errors), as well as the expressiveness of the logical languages used and the general flexibility of their application make them highly desirable (especially in the critical context); on the other hand it is expected that, as was previously the case for sequential code, automation levels will increase and render such methods more usable.
The current project has the double purpose of advancing the state of the art and providing results that can be brought to practice in the very short term by our industrial partners. Since software model checking techniques are currently much more advanced and usable in practice than deductive methods, one task of the project will be dedicated to producing a practical verification platform suited to specific needs and programming languages. On the other hand, the deduction-based approach to verification of concurrent software has become an exciting area, in which the team wants to contribute with fundamental research.
Our approach will be guided by three simples principles, as follows:
It will be incremental, starting from languages with restricted data structures and models for concurrency. This is particularly adequate for critical software, since in this area the programming languages that are used are often subject to restricted profiles that forbid less predictable behaviour.
It will combine path sensitive and path insensitive techniques, and exploit their interaction. It is our firm belief that the key to successful automatic verification lies in this combined approach.
All the methods and tools produced will be validated through real-life use cases, provided and carried out by team members who work directly in the development of embedded critical software.
We now detail our plan and the reasons why we think these three principles will lead us to successful solutions.
I.
Since C and Ada are the languages of choice in the development of embedded critical systems, we will start by addressing the
verification of concurrent programs of subsets of both languages. In
the case of Ada, the choice goes naturally to the RavenSPARK language, which has the enormous advantage of being a commercially successful product, widely used in industry, and having ideal characteristics for
our purposes: a restricted model of concurrency; restricted data structures (no aliasing is possible); an annotation language comprising assertional and dataflow contracts; and the availability of a toolset for checking both dataflow and assertions. Furthermore the team possesses experience in the verification of sequential SPARK code.
The presence of dataflow annotations, complemented by a model of concurrency that forbids the dynamic creation of threads, can be taken into account to calculate predicate abstractions of concurrent programs, since the amount of interference between threads is naturally limited by the dataflow restrictions, which can be taken for granted since they can be effectively checked by the SPARK toolset. Also, rely and guarantee conditions are intrinsically related to
dataflow annotations of individual threads of a program. It will be interesting for instance to see if such conditions can be automatically inferred from the compulsory dataflow annotations that must be present in every valid RavenSPARK program.
II.
Approaches to program verification that combine different techniques are seen as promising, even if it may be difficult for a team to
acquire the required know-how. We intend precisely to take advantage of the fact that know-how is in place, as a result of a process
carried out over the past 5 years in a number of projects, collaborations, and doctoral theses.
Predicate abstraction, which is a fundamental component of any software model checking system, is typically implemented with the help of a weakest precondition algorithm -- a deductive technique. In this project we will be in a position of deep understanding of the
deductive aspects of verification, which may allow us to produce predicate abstraction algorithms tailored to our needs. Moreover,
since the study of predicate abstractions for concurrent programs is a practically untouched field, it may well be the case that the rely-guarantee principles and verification conditions algorithms can
be used fruitfully for predicate abstraction (some published work
hints at this).
Finally, it is our conviction that a mixture of software model
checking and deductive verification can be in itself a very powerful verification method. Rely-guarantee reasoning is based on two separate aspects: "intra-thread" verification conditions for each thread
(taking as assumptions rely and guarantee conditions of all the
threads in the program), and "inter-thread" verification conditions,
to assert (compositionally) that if all threads satisfy a given
property then the ensemble does so as well. We will investigate the possibility of each of these aspects being verified by different
methods; we will for instance use a SMC to check intra-thread properties and rely-guarantee reasoning for the compositional aspect. This may still result in an acceptable level of automation in the
proofs. In the other direction we will also investigate the use of predicate abstraction itself as a tool for deductive verification at
the inter-thread level, since rely-guarantee VCs may be easier to establish for over-approximated code.
III.
This project stems from an ongoing collaboration between academics and practitioners. The team brings together
Specialists in verification from CCTC and CMAT, Univ Minho, and LIACC, Univ Porto, who will work on the theoretical aspects of all the main tasks of the project: predicate abstraction (CCTC and LIACC, task 1); properties of models (LIACC, task 2); and deductive techniques (CMAT, CCTC, and LIACC, task 3).
Researchers who are expert in embedded, safety-critical, and real-time concurrent programming, from CISTER, IPP, will work on the development of the SMC platform (task 2), provide use cases, and carry on an evaluation of the tools and methods obtained as outcomes of the project (task 4).
Main Results
The main results of the project will include (for at least one of the programming languages of interest in the safety-critical context)
a novel predicate abstraction algorithm and the corresponding implementation
a SMC toolkit for concurrent applications
a prototype generic SMC toolkit (multi-language, multi-checker)
a VCGen for rely-guarantee conditions
a general method for verification of concurrent programs combining both path-sensitive and path-insensitive techniques.
Main novelties include (i) taking advantage of specific aspects of relatively simple programming languages used in safety-critical development, and (ii) combining techniques that have not to this point been combined. Both aspects will allow us to produce tools that can be used with realistic code.
The formal verification of software is increasingly important in software engineering, particularly in the context of critical applications, which is regulated by norms that advise or enforce the use of formal or semi-formal validation techniques. Academic researchers are being led to collaborate with industry in the development of methods and tools that allow practitioners to incorporate formal verification in their validation process.
This project stems from an ongoing collaboration between three academic groups and software engineers working for companies that work precisely in safety-sensitive domains, subject to norms such as mentioned above.
After enormous developments in the verification of sequential software, industry is now able to employ formal verification
techniques in their projects, either based on model checking, abstract interpretation, or logical proofs. Unfortunately, safety-critical applications are usually inherently concurrent, which means that these are often of limited utility. Moreover, there is a mismatach between the programming languages that are receiving more attention from the research community and those that are used in practice in the safety-critical domain. Ada for instance, has paradoxically fallen out
of fashion as a general purpose programming language, but is more and more used in the safety-critical domain (a fact of which academics are seldom aware). The languages that will be object of our study will include at least a subset of C and the RavenSPARK high integrity language, both widely used by practitioners in the critical domain.
The scope of the present project is the verification of properties of
shared memory concurrent programs, both advancing the state of the art at the theoretical level and producing tools that can be used
by companies developing critical applications. Our approach will focus simultaneously on two techniques: software model checking
and deductive reasoning. Crucially, advances in each technique have historically fed back into the other technique, and we believe such a mixed approach (which is made possible by the know-how accumulated by the team over the last five years) can be fruitful.
Goals
The goals of the project are (labelled [T]heoretical or [P]ractical):
1. [T] To investigate abstraction techniques that can be used to tame the state explosion problem inherent to any programming language with a realistic set of types. For this we will build on recent work, in
particular on predicate abstraction. We hope to be able to propose enhancements to the published abstraction mechanisms, in particular stemming from the work on deductive compositional verification methods that will take place in parallel (see below).
It is not our goal to investigate model checking algorithms; our
interest is in the extraction of approximated models from the source code and in checking properties of these models using a standard model checker. This allows us to automatically take benefit from the wealth
of work accumulated on taming other sources of state explosion like control flow.
2. [P] (building on 1) To produce software model checking tools for
our object languages. The approach to be followed can be summarized as follows: we will perform syntactical analysis of the source code, and apply abstraction techniques to obtain the control flow graph of an approximated version of the initial program. From this we will produce
a Labelled Transitions (LT) model. The tool will also translate properties (expressed as comments
in the source code) to properties expressed in the logic of the model checker, that
can be used to query it.
3. [P] (building on 2) To investigate the possibility of producing a common language for representing LT systems and properties of these systems. The idea would be that these models and properties can then be exported to more than one model checking tool. It may well be the case that some properties can be checked with one model checker, while another checker may be able to check other properties. In this generic approach we take inspiration from tools for deductive verification of sequential programs, like Why and Boogie.
4. [T,P] To propose a verification conditions generator (VCGen) for a (concurrent) subset of one of our object languages, based on rely-guarantee principles. The subset will be sufficiently simple to allow us to focus on the generation of verification conditions, and to put together a complete verification platform, consisting of the VCGen and a choice of SMT solvers to discharge the VCs.
5. [T] (building on 4) To study extensions of the rely-guarantee
system to accommodate progressively richer features of the programming language, including heap-based dynamic structures. We will consider in particular combinations with formalisms like separation logic and
typed memory.
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
TWiki's Research/Aviacc webThe Research/Aviacc web of TWiki. TWiki is a Web-Based Collaboration Platform for the Enterprise.http://wiki.di.uminho.pt/twiki/bin/view/Research/AviaccCopyright 2020 by contributing authors2016-01-04T18:00:54ZPublicationshttp://wiki.di.uminho.pt/twiki/bin/view/Research/Aviacc/Publications2016-01-04T18:00:54ZCurrently submitted André de Matos Pedro, David Pereira, Luís Miguel Pinho, and Jorge Sousa Pinto. Monitoring for a decidable fragment of MTL #1113091;S. Submitted ... (last changed by JorgeSousaPinto)JorgeSousaPintoToolshttp://wiki.di.uminho.pt/twiki/bin/view/Research/Aviacc/Tools2015-05-20T09:17:14ZSoftware Tools and Packages HSMTlib A Haskell library for easy interaction with multiple SMT solvers. Available through Hackage. SPARK parser A parser library for ... (last changed by JorgeSousaPinto)JorgeSousaPintoWebSideBarhttp://wiki.di.uminho.pt/twiki/bin/view/Research/Aviacc/WebSideBar2015-05-19T13:20:29ZOverview Home Project Proposal Team Research Team Job Opportunities Results Publications Tools Events First Project Meeeting ... (last changed by JorgeSousaPinto)JorgeSousaPinto2ndWorkshophttp://wiki.di.uminho.pt/twiki/bin/view/Research/Aviacc/2ndWorkshop2015-05-19T13:19:43ZAVIACC Second Meeting and Workshop Date September 16, 2013, 10:00 Place DCC FCUP, videoconference room Schedule 10h00 12h30: Scientific talks and discussion 14h30 ... (last changed by JorgeSousaPinto)JorgeSousaPinto1stWorkshophttp://wiki.di.uminho.pt/twiki/bin/view/Research/Aviacc/1stWorkshop2015-05-19T13:19:33ZAVIACC First Project Meeting Date December 18, 2012, 10:00 Place DCC FCUP, videoconference room Schedule 10h00 11h30: Scientific talks and discussion 11h30 ... (last changed by JorgeSousaPinto)JorgeSousaPintoJobshttp://wiki.di.uminho.pt/twiki/bin/view/Research/Aviacc/Jobs2014-04-23T11:17:00ZBI Grant Announcements of a Bounded Model Checker for SPARK closed Abstraction for Critical Programs closed and tools for the analysis and verification ... (last changed by JorgeSousaPinto)JorgeSousaPintoTeamhttp://wiki.di.uminho.pt/twiki/bin/view/Research/Aviacc/Team2014-04-23T11:07:22ZSenior Researchers Sabine Broda FCUP Daniela da Cruz UM Maria João Frade UM Nelma Moreira FCUP David Pereira IPP Luís Miguel ... (last changed by JorgeSousaPinto)JorgeSousaPintoWebHomehttp://wiki.di.uminho.pt/twiki/bin/view/Research/Aviacc/WebHome2014-04-22T15:30:07ZAnalysis and Verification of Critical Concurrent Programs The scope of the present project is the verification of properties of safety critical software. Our approach ... (last changed by JorgeSousaPinto)JorgeSousaPintoDescriptionhttp://wiki.di.uminho.pt/twiki/bin/view/Research/Aviacc/Description2013-02-20T11:22:26ZMotivation In a brief comparison of software model checking with deductive verification techniques for the purpose of verifying concurrent software, we stress the ... (last changed by JorgeSousaPinto)JorgeSousaPintoProjectSummaryhttp://wiki.di.uminho.pt/twiki/bin/view/Research/Aviacc/ProjectSummary2013-02-18T18:51:40ZProject Summary The formal verification of software is increasingly important in software engineering, particularly in the context of critical applications, which ... (last changed by JorgeSousaPinto)JorgeSousaPintoWebPreferenceshttp://wiki.di.uminho.pt/twiki/bin/view/Research/Aviacc/WebPreferences2013-02-18T17:30:17ZResearch/Aviacc Web Preferences The following settings are web preferences of the Research/Aviacc web. These preferences overwrite the site level preferences ... (last changed by JorgeSousaPinto)JorgeSousaPintoNewshttp://wiki.di.uminho.pt/twiki/bin/view/Research/Aviacc/News2013-01-10T14:59:52ZThe first project meeting took place on December 18 2012, at FCUP. (last changed by JorgeSousaPinto)JorgeSousaPintoWebStatisticshttp://wiki.di.uminho.pt/twiki/bin/view/Research/Aviacc/WebStatistics2012-12-20T06:57:54ZStatistics for Research/Aviacc Web Month: Topic views: Topic saves: File uploads: Most popular topic views: Top contributors for topic ... (last changed by TWikiGuest)TWikiGuestWebTopicListhttp://wiki.di.uminho.pt/twiki/bin/view/Research/Aviacc/WebTopicList2006-11-15T19:43:52Z (last changed by TWikiContributor)TWikiContributorWebSearchAdvancedhttp://wiki.di.uminho.pt/twiki/bin/view/Research/Aviacc/WebSearchAdvanced2006-11-15T19:43:52Z (last changed by TWikiContributor)TWikiContributorWebTopicCreatorhttp://wiki.di.uminho.pt/twiki/bin/view/Research/Aviacc/WebTopicCreator2006-11-15T19:43:52Z (last changed by TWikiContributor)TWikiContributor
Currently submitted André de Matos Pedro, David Pereira, Luís Miguel Pinho, and Jorge Sousa Pinto. Monitoring for a decidable fragment of MTL #1113091;S. Submitted ...
Software Tools and Packages HSMTlib A Haskell library for easy interaction with multiple SMT solvers. Available through Hackage. SPARK parser A parser library for ...
AVIACC Second Meeting and Workshop Date September 16, 2013, 10:00 Place DCC FCUP, videoconference room Schedule 10h00 12h30: Scientific talks and discussion 14h30 ...
AVIACC First Project Meeting Date December 18, 2012, 10:00 Place DCC FCUP, videoconference room Schedule 10h00 11h30: Scientific talks and discussion 11h30 ...
BI Grant Announcements of a Bounded Model Checker for SPARK closed Abstraction for Critical Programs closed and tools for the analysis and verification ...
Analysis and Verification of Critical Concurrent Programs The scope of the present project is the verification of properties of safety critical software. Our approach ...
Motivation In a brief comparison of software model checking with deductive verification techniques for the purpose of verifying concurrent software, we stress the ...
Project Summary The formal verification of software is increasingly important in software engineering, particularly in the context of critical applications, which ...
Research/Aviacc Web Preferences The following settings are web preferences of the Research/Aviacc web. These preferences overwrite the site level preferences ...
Analysis and Verification of Critical Concurrent Programs
The scope of the present project is the verification of properties of safety-critical software. Our approach will focus simultaneously on two techniques: software model checking and deductive reasoning, both advancing the state of the art at the theoretical level and producing tools that can be used by companies developing critical applications. We are particularly interested in interactions between both approaches, which have historically fed back into each other.
One particular topic that will be investigated is the formal verification of shared memory concurrent programs, elucidating the feasibility of their use in the safety-critical context.
(read more)
Project info
Este trabalho é financiado por Fundos FEDER através do Programa Operacional Fatores de Competitividade - COMPETE e por Fundos Nacionais através da FCT - Fundação para a Ciência e a Tecnologia no âmbito do projeto FCOMP-01-0124-FEDER-020486
This work is funded by ERDF - European Regional Development Fund through the COMPETE Programme (operational programme for competitiveness) and by National Funds through the FCT - Fundação para a Ciência e a Tecnologia (Portuguese Foundation for Science and Technology) within project FCOMP-01-0124-FEDER-020486
Supported by
under contract PTDC/EIA-CCO/108995/2008 (94 KEuro)
AVIACC First Project Meeting Date December 18, 2012, 10:00 Place DCC FCUP, videoconference room Schedule 10h00 11h30: Scientific talks and discussion 11h30 ...
AVIACC Second Meeting and Workshop Date September 16, 2013, 10:00 Place DCC FCUP, videoconference room Schedule 10h00 12h30: Scientific talks and discussion 14h30 ...
Motivation In a brief comparison of software model checking with deductive verification techniques for the purpose of verifying concurrent software, we stress the ...
BI Grant Announcements of a Bounded Model Checker for SPARK closed Abstraction for Critical Programs closed and tools for the analysis and verification ...
Project Summary The formal verification of software is increasingly important in software engineering, particularly in the context of critical applications, which ...
Currently submitted André de Matos Pedro, David Pereira, Luís Miguel Pinho, and Jorge Sousa Pinto. Monitoring for a decidable fragment of MTL #1113091;S. Submitted ...
Software Tools and Packages HSMTlib A Haskell library for easy interaction with multiple SMT solvers. Available through Hackage. SPARK parser A parser library for ...
Analysis and Verification of Critical Concurrent Programs The scope of the present project is the verification of properties of safety critical software. Our approach ...
Research/Aviacc Web Preferences The following settings are web preferences of the Research/Aviacc web. These preferences overwrite the site level preferences ...
This is a subscription service to be automatically notified by e-mail when topics change in this Research/Aviacc web. This is a convenient service, so you do not have to come back and check all the time if something has changed. To subscribe, please add a bullet with your WikiName in alphabetical order to this list:
Each TWiki web has an automatic e-mail notification service that sends you an e-mail with links to all of the topics modified since the last alert.
Users subscribe to email notifications using their WikiName or an alternative email address, and can specify the webs/topics they wish to track using one of these bullet list formats:
three spaces * [ webname . ] wikiName - SMTP mail address three spaces * [ webName . ] wikiName three spaces * SMTP mail address three spaces * SMTP mail address : topics three spaces * [ webname . ] wikiName : topics
In the above examples, topics is a space-separated list of topic names. The user may further customize the specific content they will receive using the following formats:
Specify topics without a Web. prefix
Topics must exist in this web.
Topics may be specified using * wildcards
Each topic may optionally be preceded by a '+' or '-' sign. The '+' sign means "subscribe to this topic" (the same as not putting anything). The '-' sign means "unsubscribe" or "don't send notifications regarding this topic". This allows users to elect to filter out certain topics (and their children, to an arbitrary depth). Topic filters ('-') take precedence over topic includes ('+').
Each topic may optionally be followed by an integer in parentheses, indicating the depth of the tree of children below that topic. Changes in all these children will be detected and reported along with changes to the topic itself. Note This uses the TWiki "Topic parent" feature.
Each topic may optionally be immediately followed by an exclamation mark ! or a question mark ? with no intervening spaces, indicating that the topic (and children if there is a tree depth specifier as well) should be mailed out as complete topics instead of change summaries. ! causes the topic to be mailed every time even if there have been no changes, ? will mail the topic only if there have been changes to it. This only makes sense for subscriptions.
For example:
Subscribe Daisy to all changes to topics in this web.
* daisy.cutter@flowers.com
Subscribe Daisy to all changes in all webs that start with Web.
* daisy.cutter@flowers.com: Web*
Subscribe Daisy to changes to topics starting with Petal, and their immediate children, WeedKillers and children to a depth of 3, and all topics that match start with Pretty and end with Flowers e.g. PrettyPinkFlowers
Subscribe Daisy to the full content of NewsLetter whenever it has changed
* daisy@flowers.com: TWiki.NewsLetter?
Subscribe buttercup to NewsLetter and its immediate children, even if it hasn't changed.
* buttercup@flowers.com: TWiki.NewsLetter! (1)
Subscribe GardenGroup (which includes Petunia) to all changed topics under AllnewsLetters to a depth of 3. Then unsubscribe Petunia from the ManureNewsLetter, which she would normally get as a member of GardenGroup? :
A user may be listed many times in the WebNotify topic. Where a user has several lines in WebNotify that all match the same topic, they will only be notified about changes that topic once (though they will still receive individual mails for news topics).
If a TWiki group is listed for notification, the group will be recursively expanded to the e-mail addresses of all members.
Tip: List names in alphabetical order to make it easier to find the names.
Note for System Administrators: Notification is supported by an add-on to the TWiki kernel called the MailerContrib. See the MailerContrib topic for details of how to set up this service.
Note: If you prefer a news feed, point your reader to WebRss (for RSS 1.0 feeds) or WebAtom (for ATOM 1.0 feeds). Learn more at WebRssBase and WebAtomBase, respectively.
Related topics:WebChangesAlert, TWikiUsers, TWikiRegistration
These settings override the defaults for this web only. See full list of defaults with explanation. Many of the settings below are commented out. Remove the # sign to enable a local customisation.
Web-specific background color: (Pick a lighter one of the StandardColors).
Set WEBBGCOLOR = #D0D0D0
Note: This setting is automatically configured when you create a web
Image, URL and alternate tooltip text of web's logo. Note: Don't add your own local logos to the TWikiLogos topic; create your own logos topic instead.
List this web in the SiteMap. If you want the web listed, then set SITEMAPLIST to on, do not set NOSEARCHALL, and add the "what" and "use to..." description for the site map. Use links that include the name of the web, i.e. Research/Aviacc.Topic links. Note: Unlike other variables, the setting of SITEMAPLIST is not inherited from parent webs. It has to be set in every web that is to be listed in the SiteMap
Set SITEMAPLIST = on
Set SITEMAPWHAT = Projeto AVIACC
Set SITEMAPUSETO = Analysis and Verification of Critical Concurrent Programs
Note: Above settings are automatically configured when you create a web
Exclude web from a web="all" search: (Set to on for hidden webs).
Set NOSEARCHALL =
Note: This setting is automatically configured when you create a web
Prevent automatic linking of WikiWords and acronyms (if set to on); link WikiWords (if empty); can be overwritten by web preferences:
#Set NOAUTOLINK =
Note: You can still use the [[...][...]] syntax to link topics if you disabled WikiWord linking. The <noautolink> ... </noautolink> syntax can be used to prevents links within a block of text.
Default template for new topics for this web:
WebTopicEditTemplate? : Default template for new topics in this web. (Site-level is used if topic does not exist)
Comma separated list of forms that can be attached to topics in this web. See TWikiForms for more information.
Set WEBFORMS =
Users or groups who are not / are allowed to view / change / rename topics in the Research/Aviacc web: (See TWikiAccessControl). Remove the # to enable any of these settings. Remember that an empty setting is a valid setting; setting DENYWEBVIEW to nothing means that anyone can view the web.
Preferences are used as TWikiVariables by enclosing the name in percent signs. Example:
When you write variable %WEBBGCOLOR% , it gets expanded to #D0D0D0
The sequential order of the preference settings is significant. Define preferences that use other preferences first, i.e. set WEBCOPYRIGHT before WIKIWEBMASTER since %WEBCOPYRIGHT% uses the %WIKIWEBMASTER% variable.
You can introduce your own preferences variables and use them in your topics and templates.
TWiki search results for \.*
http://wiki.di.uminho.pt/twiki/bin/view/Research/Aviacc
The Research/Aviacc web of TWiki. TWiki is a Web-Based Collaboration Platform for the Enterprise.en-usCopyright 2020 by contributing authorsTWiki Administrator [webmaster@di.uminho.pt]The contributing authors of TWikiTWikiDIUM.Research/Aviacc
http://wiki.di.uminho.pt/twiki/bin/view/Research/Aviacc
/twiki/pub/Main/LocalLogos/um_eengP.jpgPublications
http://wiki.di.uminho.pt/twiki/bin/view/Research/Aviacc/Publications
Currently submitted André de Matos Pedro, David Pereira, Luís Miguel Pinho, and Jorge Sousa Pinto. Monitoring for a decidable fragment of MTL #1113091;S. Submitted ... (last changed by JorgeSousaPinto)2016-01-04T18:00:54ZJorgeSousaPintoTools
http://wiki.di.uminho.pt/twiki/bin/view/Research/Aviacc/Tools
Software Tools and Packages HSMTlib A Haskell library for easy interaction with multiple SMT solvers. Available through Hackage. SPARK parser A parser library for ... (last changed by JorgeSousaPinto)2015-05-20T09:17:14ZJorgeSousaPintoWebSideBar
http://wiki.di.uminho.pt/twiki/bin/view/Research/Aviacc/WebSideBar
Overview Home Project Proposal Team Research Team Job Opportunities Results Publications Tools Events First Project Meeeting ... (last changed by JorgeSousaPinto)2015-05-19T13:20:29ZJorgeSousaPinto2ndWorkshop
http://wiki.di.uminho.pt/twiki/bin/view/Research/Aviacc/2ndWorkshop
AVIACC Second Meeting and Workshop Date September 16, 2013, 10:00 Place DCC FCUP, videoconference room Schedule 10h00 12h30: Scientific talks and discussion 14h30 ... (last changed by JorgeSousaPinto)2015-05-19T13:19:43ZJorgeSousaPinto1stWorkshop
http://wiki.di.uminho.pt/twiki/bin/view/Research/Aviacc/1stWorkshop
AVIACC First Project Meeting Date December 18, 2012, 10:00 Place DCC FCUP, videoconference room Schedule 10h00 11h30: Scientific talks and discussion 11h30 ... (last changed by JorgeSousaPinto)2015-05-19T13:19:33ZJorgeSousaPintoJobs
http://wiki.di.uminho.pt/twiki/bin/view/Research/Aviacc/Jobs
BI Grant Announcements of a Bounded Model Checker for SPARK closed Abstraction for Critical Programs closed and tools for the analysis and verification ... (last changed by JorgeSousaPinto)2014-04-23T11:17:00ZJorgeSousaPintoTeam
http://wiki.di.uminho.pt/twiki/bin/view/Research/Aviacc/Team
Senior Researchers Sabine Broda FCUP Daniela da Cruz UM Maria João Frade UM Nelma Moreira FCUP David Pereira IPP Luís Miguel ... (last changed by JorgeSousaPinto)2014-04-23T11:07:22ZJorgeSousaPintoWebHome
http://wiki.di.uminho.pt/twiki/bin/view/Research/Aviacc/WebHome
Analysis and Verification of Critical Concurrent Programs The scope of the present project is the verification of properties of safety critical software. Our approach ... (last changed by JorgeSousaPinto)2014-04-22T15:30:07ZJorgeSousaPintoDescription
http://wiki.di.uminho.pt/twiki/bin/view/Research/Aviacc/Description
Motivation In a brief comparison of software model checking with deductive verification techniques for the purpose of verifying concurrent software, we stress the ... (last changed by JorgeSousaPinto)2013-02-20T11:22:26ZJorgeSousaPintoProjectSummary
http://wiki.di.uminho.pt/twiki/bin/view/Research/Aviacc/ProjectSummary
Project Summary The formal verification of software is increasingly important in software engineering, particularly in the context of critical applications, which ... (last changed by JorgeSousaPinto)2013-02-18T18:51:40ZJorgeSousaPintoWebPreferences
http://wiki.di.uminho.pt/twiki/bin/view/Research/Aviacc/WebPreferences
Research/Aviacc Web Preferences The following settings are web preferences of the Research/Aviacc web. These preferences overwrite the site level preferences ... (last changed by JorgeSousaPinto)2013-02-18T17:30:17ZJorgeSousaPintoNews
http://wiki.di.uminho.pt/twiki/bin/view/Research/Aviacc/News
The first project meeting took place on December 18 2012, at FCUP. (last changed by JorgeSousaPinto)2013-01-10T14:59:52ZJorgeSousaPintoWebChanges
http://wiki.di.uminho.pt/twiki/bin/view/Research/Aviacc/WebChanges
(last changed by TWikiContributor)2006-11-15T19:43:52ZTWikiContributorWebIndex
http://wiki.di.uminho.pt/twiki/bin/view/Research/Aviacc/WebIndex
(last changed by TWikiContributor)2006-11-15T19:43:52ZTWikiContributorWebSearch
http://wiki.di.uminho.pt/twiki/bin/view/Research/Aviacc/WebSearch
(last changed by TWikiContributor)2006-11-15T19:43:52ZTWikiContributorWebSearchAdvanced
http://wiki.di.uminho.pt/twiki/bin/view/Research/Aviacc/WebSearchAdvanced
(last changed by TWikiContributor)2006-11-15T19:43:52ZTWikiContributor
Research/Aviacc Web
Create New Topic
Index
Search
Changes
Notifications
Statistics
Preferences
DI
Tip: List names in alphabetical order to make it easier to find the names.
Note for System Administrators: Notification is supported by an add-on to the TWiki kernel called the MailerContrib. See the 
Rename, move or delete this web: 
If you already know the name of the topic, enter the name of the topic into the 
List topics that start with the letter: 
Once you have created the topic, consider adding links in related topics to the new topic so that there are more ways people can discover it.
Copyright © by the contributing authors. Ideas, requests, problems? Send feedback.