PhD Opportunities

• Domain-specific Program Verification Infrastructures: proposed by JoseBacelarAlmeida and JorgeSousaPinto in the context of the MAPi doctoral programme.

Master Opportunities

Automated Model checking in ADA/Spark Topic: Model checking for real-time systems allows to ensure that a system (the model) verifies the required temporal properties. To be useful, the model must be automatically inferred/translated from the system source code. In the scope of the RESCUE project, it was developed a translation from HTL (a coordination language for concurrent real-time systems) to timed-automata networks of the UPPAAL system. Based on this experience, it is intended to extend/adapt this framework To the ADA/Spark language. The work will include the construction of a translator able to abstract ADA tasks coordination and provide a model for which temporal properties can be analysed.

Call closes on November 12, 2009. To apply see www.eracareers.pt.

For more information contact nam@ncc.up.pt or desousa@di.ubi.pt.

Research Training Opportunities

• bolsaRescue0909.pdf: ADA/SPARK model checking

Books

• José Carlos Bacelar Almeida, Maria João Frade, Jorge Sousa Pinto, Simão Melo de Sousa. Rigorous Software Development, An Introduction to Program Verification. Series: Undergraduate Topics in Computer Science, Springer. 1st Edition., 2011, XIII, 307 p. 52 illus. ISBN: 978-0-85729-017-5.

• Simão Melo de Sousa. Outils et Techniques pour la verification formelle da la plateforme Javacard. Édition Universitaires Européenes. February 2011. ISBN: 978-613-1-53931-2.

Papers in Journals

2011

• J. Espírito Santo, A note on preservation of strong normalisation in the lambda-calculus. Theoretical Computer Science 412(11): 1027-1032, 2011.

• J. Espírito Santo, L. Pinto. A calculus of multiary sequent terms. To appear in ACM Transactions on Computational Logic. 2011.

• M. J. Frade, J. S. Pinto. Verification Conditions for Source-level Imperative Programs. In Computer Science Review, Volume 5, Issue 2, 2011. Elsevier. DOI:10.1016/ j.cosrev.2011.02.002.

• Jose Bernardo Barros, Daniela da Cruz, Pedro Rangel Henriques, and Jorge Sousa Pinto. Assertion-based Slicing and Slice Graphs. To appear in Formal Aspects of Computing, 2011.

• Sabine Broda, António Machiavelo, Nelma Moreira, and Rogério Reis. On the average state complexity of partial derivative automata. International Journal of Foundations of Computer Science, 2011.

• Sandra Alves, Maribel Fernandez, Mario Florido and Ian Mackie. Linearity and Iterator Types for Godel's System T. To appear in International Journal on Higher-Order and Symbolic Computation, Springer. 2011.

2010

• J. Almeida, M. Barbosa, J. Pinto, and B. Vieira. Deductive Verification of Cryptographic Software. Innovations in Systems and Software Engineering - a NASA Journal - 6(3): 203-218 Springer, 2010.

• Sandra Alves, Maribel Fernandez, Mário Florido and Ian Mackie. Goedel's System T Revisited. Theoretical Computer Science, Elsevier Science, 2010.

2009

• J. Esprito Santo. The Lambda-Calculus and the Unity of Structural Proof Theory. Special Issue on Computability in Europe 2007, Theory of Computing Systems, 45:963-994, 2009

• Nuno Gaspar and Simão Melo de Sousa. WebVm - A web-based host platform for pedagogical virtual machines, INFORMÁTICA NA EDUCAÇÃO: teoria e prática. Porto Alegre, vol.12, n.1, jan./jun. 2009. ISSN digital 1982-1654, ISSN imp. 1516-084X (journal version of the IFIP-WCCE paper).

2008

• Simão Melo de Sousa, Guest editorial of Journal of Computer Science and Information Systems, Special Issue on Compilers, Related Technologies and Applications. Volume 5, Number 2, December 2008 ISSN: 1820-0214..

• Maria João Varanda, Pedro Rangel Henriques, Simão Melo de Sousa (Eds.). Proceedings of the conference Corta'08 "COmpilers, Related Technologies and Applications". IPB Publisher, 2008. ISBN:978-972-745-096-1. Edição de actas de conferência nacional.

• David Pereira and Nelma Moreira. KAT and PHL in Coq (extended version). ComSIS journal (Computer Science and Information Systems), Volume 05, Issue 02 (December 2008). ISSN: 1820-0214.

Papers in Workshops and Conferences

2011

• Nuno Gaspar, Vítor Gonçalves Rodrigues,Simão Melo de Sousa. Cerifying Execution Time. Foundational and Practical Aspects of Ressource Analysis. FOPARA'2011, May 2011, Madrid Spain.

• Vítor Gonçalves Rodrigues, Mário Florido, Simão Melo de Sousa. A Functional Approach to Worst-Case Execution Time Analysis. Functional and (Constraint) Logic Programming - WFLP'2011. July 2011, Odense , Denmark.

2010

• J. Espírito Santo, Towards a canonical classical natural deduction system, in A. Dawar, H. Veith (Eds.), 19th EACSL International Conference Computer Science Logic (CSL 2010), Lecture Notes in Computer Science, Springer, vol. 6247, 2010.

• Eduardo Brito and Jorge Sousa Pinto. Program Verification in SPARK and ACSL: A Comparative Case Study - 15th International Conference on Reliable Software Technologies - Ada-Europe 2010.

• Daniela da Cruz, Pedro Rangel Henriques and Jorge Sousa Pinto GamaSlicer? : an Online Laboratory for Program Verification and Analysis. Proceedings of the of the Tenth Workshop on Language Descriptions, Tools and Applications, LDTA 2010, Paphos, Cyprus, March 28-29, 2010.

• Daniela da Cruz, Pedro Rangel Henriques, Jorge Sousa Pinto. Contract-Based Slicing. Proceedings of the 4th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISOLA'2010), p106-120. 18-20 October 2010 - Amirandes, Heraclion, Crete. Lecture Notes in Computer Science (LNCS-6415), Springer Verlag.

• José Bacelar Almeida, Nelma Moreira, David Pereira, and Simão Melo de Sousa. Partial derivative automata formalized in Coq. In Proceedings of the 15th International Conference on Implementation and Application of Automata (CIAA 2010), number 6482 in Lecture Notes on Computer Science, pages 59-68, Winnipeg, MA, Canada, August, 2010. 2011. Springer-Verlag.

• Sabine Broda, António Machiavelo, Nelma Moreira, and Rogério Reis. On the average number of states of partial derivative automata. In Yuan Gao, Hanlin Lu, Shinnosuke Seki, and Sheng Yu, editors, Developments in Language Theory, 14th International Conference, DLT 2010, London, ON, Canada, August 17-20, 2010. Proceedings, volume 6224 of Lecture Notes on Computer Science, pages 112-123, London, ON, Canada, August 2010. Springer-Verlag. DOI:10.1007/978-3-642-14455-4 12.

• Eva Maia, Nelma Moreira, and Rogério Reis. Inferência de tipos em Python. In Luís S. Barbosa and Miguel P. Correia, editors, Inforum, Simpósio de Informática, pages 515-518, Braga,Portugal, 9-10 Setembro 2010.

• Maia, C., Nogueira, L., Pinho, L., Evaluating Android OS for Embedded Real-Time Systems, Published in Proceedings of the 6th International Workshop on Operating Systems Platforms for Embedded Real-Time Applications, Brussels, Belgium, July 2010. pp. 63-70.

• Maia, C., Nogueira, L., Pinho, L., Short Paper: Experiences on the Implementation of a Cooperative Embedded System Framework, Published in Proceedings of the 8th International Workshop on Java Technologies for Real-Time and Embedded Systems, Prague, Czech Republic, August 2010. pp. 70-72.

• Gonçalves, J., Ferreira, L., A Framework for QoS-Aware Service-based Mobile Systems, Published at Inforum 2010. II Simpósio de Informática, Luís S. Barbosa, Miguel P. Correia (eds), Braga, 9-10 Setembro, 2010, pp. 711.

• Gonçalves, J., Ferreira, L., Pinho, L., Silva, G., Handling Mobility on a QoS-Aware Service-based Framework for Mobile Systems, 2010 IEEE/IFIP International Conference on Embedded and Ubiquitous Computing, Hong-Kong, China, Dec 2010, pp. 97 - 104.

• Barros, A., Pinho, L., Managing contention of software transactional memory in real-time systems, Work in Progress (WiP) session of the 31st IEEE Real-Time Systems Symposium (RTSS 2010), San Diego, CA, USA, November 30 - December 3, 2010.

• André Carvalho, Joel Carvalho, Jorge Sousa Pinto, Simão Melo de Sousa. Model-Checking Temporal Properties of Real-Time HTL Programs. Proceedings of the 4th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISOLA'2010) 18-20 October 2010 - Amirandes, Heraclion, Crete. Lecture Notes in Computer Science (LNCS-6415), Springer Verlag.

• Nuno Gaspar, Rogério Reis and Simão Melo de Sousa. Timing Analysis - From Predictions to Certificates (nominated for the best student paper award). Actas do II Simpósio de Informática. INForum'2010. Universidade do Minho, Braga, 9-10 Setembro, 2010. Luís S. Barbosa, Miguel P. Correia (Eds.). P

• Joaquim Tojal, Carlos Carloto, José Faria and Simão Melo de Sousa. Towards a Formally Verified Kernel Module. Actas do II Simpósio de Informática. INForum'2010. Universidade do Minho, Braga, 9-10 Setembro, 2010. Luís S. Barbosa, Miguel P. Correia (Eds.).

• Diogo Fialho, Nuno Gaspar, Jorge Sousa Pinto, Rogério Reis, Simão Melo de Sousa. Towards a Worst-Case Execution Time Calculation Platform with Certificate Production. Proceedings of EDCC'2010, Valencia, Spain.

• Simão Melo de Sousa. Design by Contracts approach to the formal verification of programs. Invited talk. Tech'Days 2010, Lisbon - Portugal. April 2010.

• Simão Melo de Sousa. An introduction to program logic and the formal development of software. Invited talk. Days in Logic' 2010, Porto - Portugal. January 2010.

• D. Fialho , N. Gaspar, J. S.Pinto, R. Reis and S. Melo de Sousa. Worst-Case Execution Time: From predictions to certificates. Proceedings of the Days in Logic'2010. Porto - Portugal. January 2010.

• N. Moreira, D. Pereira and S. Melo de Sousa. Deciding regular expressions equivalence in Coq. Proceedings of the Days in Logic'2010. Porto - Portugal. January 2010.

• V. Rodrigues, M. Florido and S. Melo de Sousa. Pragmatic Program Transformation and Verification: an Abstract Interpretation Perspective. Proceedings of the Days in Logic'2010. Porto - Portugal. January 2010.

2009

• M. J. Frade, A. Saabas, T. Uustalu, Bidirectional data- ow analyses, type-systematically, PEPM09, ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, Savannah, Georgia, USA, January 19-20, 2009.

• J. B. Almeida, M. Barbosa, J. S. Pinto, and B. Vieira. Verifying Cryptographic Software Correctness with Respect to Reference Implementations. In M. Alpuente, B. Cook, and C. Joubert, editors, Proceedings of the 4th International Workshop on Formal Methods for Industrial Critical Systems (FMICS'2009), volume 5825 of Lecture Notes in Computer Science, pages 37-52. Springer, 2009. Distinguished with the Best Paper award, from EASST.

• J. B. Almeida, M. Barbosa, J. S. Pinto, and B. Vieira. Deductive Verification of Cryptographic Software. In Proceedings of the First NASA Formal Methods Symposium (NFM 2009), NASA conference publication CP-2009-215407.

• Marco Almeida, Nelma Moreira, and Rogèrio Reis. Testing equivalence of regular languages. In Workshop on Descriptional Complexity of Formal Systems (DCFS09), Magdeburg, Germany, July 2009. Also in Electronic Proceedings in Theoretical Computer Science (eptcs 3) http://www.eptcs.org. DOI: 10.4204/EPTCS.3.4.

• D. Pereira. Encoding Kleene algebra (with tests) in Coq. Presentations session of the 18th EACSL Annual Conference on Computer Science Logic, CSL' 09 , Coimbra, Portugal, Sept. 2009.

• Nogueira, L., Pinho, L., Coelho, J., Coordinated Runtime Adaptations in Cooperative Open Real-Time Systems, Published in the 7th IEEE/IFIP International Conference on Embedded and Ubiquitous Computing, Aug. 2009, Vancouver, Canadá.

• Joel Silva Carvalho and Simão Melo de Sousa. Verificação de Modelos em Programas HTL, INFORUM 2009 proceedings, Lisbon. September 2009.

• André Passos, José Miguel Faria, Simão Melo de Sousa. Assessing the Formal Development of a Secure Partitioning Kernel with the B Method. ESA Workshop on Avionics Data, Control and Software Systems (ADCSS 2009) - Tracks on Formal Methods in Software Engineering.

• Nuno Gaspar and Simão Melo de Sousa. WebVm - A web-based host platform for pedagogical virtual machines, Proceedings of the IFIP WCCE - Bento Gonçalves, Brazil, July 2009.

2008

• J. Esprito Santo. The Lambda-Calculus and the Unity of Structural Proof Theory. Computability in Europe, 2008 (an extended version appears as a journal paper).

• L. Pinto, T. Uustalu. Proof search and counter-model construction for bi-intuitionistic propositional logic with labelled sequents, in M. Giese, A. Waaler (Eds.), Automated Reasoning with Analytic Tableaux and Related Methods, 18th International Conference TABLEAUX 2009, Lecture Notes in Computer Science, volume 5607, pp. 295-309, Springer, 2009.

• J. Esprito Santo, S. Ghilezan, J. Ivetic. Characterizing strongly normalizing intuitionistic sequent terms. In M. Miculan, I. Scagnetto, F. Honsell (Eds.), Types for Proofs and Programs, International Conference TYPES 2007, Revised Selected Papers, Lecture Notes in Computer Science, volume 4941, pp. 85-99, Springer, 2008.

• Diogo Fialho and Jorge Sousa Pinto, A comparative study of verification condition generators. In proceedings of Compilers, Related Technologies and and Applications (CoRTA2008)

• Daniela da Cruz, Pedro Rangel Henriques, and Jorge Sousa Pinto, Properties preservation during transformation. In proceedings of Compilers, Related Technologies and and Applications (CoRTA2008)

• David Pereira and Nelma Moreira. Kat and PHL in COQ. In proceedings of Compilers, Related Technologies and and Applications (CoRTA2008)

• Nuno Gaspar. Learning, teaching, playing with compiler construction - A web based host platform for target virtual machines. Proceedings of CoRTA'2008, IPB press,ISBN 978-972-745-096-1.

• David Pereira and Nelma Moreira. Ebdi in Coq. Days in Logic, 2008. Lisboa, Portugal, 2008.

• David Pereira, Eugenio Oliveira, and Nelma Moreira. Formal modelling of emotions in Ebdi agents. In Eightth Workshop on Computational Logic in Multi-Agent Systems (CLIMA-VIII), LNAI, Porto, Portugal, 2008. Springer-Verlag.

• Sandra Alves, Mário Florido, Ian Mackie and François-Régis Sinot. Minimality in a Linear Calculus with Iteration. The 7th International Workshop on Reduction Strategies in Rewriting and Programming (WRS), Electr. Notes Theor. Comput. Sci. 204: 163-179, 2008.

• Nogueira, L., Pinho, L., Handling QoS Dependencies in Distributed Cooperative Real-Time Systems, Published in Proceedings of the 6th IFIP Working Conference on Distributed and Parallel Embedded Systems, Milan, Italy, September 2008.

• Nogueira, L., Pinho, L., Dynamic QoS Adaptation of Inter-Dependent Task Sets in Cooperative Embedded Systems, Published in Proceedings of the 2nd ACM International Conference on Autonomic Computing and Communication Systems, Turin, Italy, September 2008.

• M. Barbosa, T. Brouard, S. Cauchie, S. Melo de Sousa. Secure Biometric Authentication with Improved Accuracy. ACISP 2008: 21-36. Lecture Notes in Computer Science 5107 Springer. 2008, ISBN 978-3-540-69971-2.

Tehcnical Reports

2010

• André Carvalho, Nuno Silva, Simão Melo de Sousa, and Nelma Moreira. A tool for automatic model extraction of ada/spark programs. Technical

2009

• Marco Almeida, Nelma Moreira, Rogèrio Reis. Testing Regular Languages Equivalence. Technical Report DCC-2009-01, DCC - FC & LIACC, Universidade do Porto, 06/2009.

• Nelma Moreira, David Pereira, Simão Melo de Sousa. On the mechanization of Kleene algebra in Coq. Technical Report DCC-2009-03, DCC - FC & LIACC, Universidade do Porto, 04/2009.

2008

• Nelma Moreira, David Pereira and Simão Melo de Sousa. Mobile code security based on Kleene algebras and temporal logics. Technical Report DCC-2008-04, DCC - FC & LIACC, Universidade do Porto, August 2008.

• Maria João Frade and Jorge Sousa Pinto, Verification conditions for source-level imperative programs. Technical Report DI-CCTC-08-01, Computer Science and Technology Center, Universidade do Minho, 2008

.natRevision { width:0px; height:0px; overflow:hidden; }

.natBreadCrumbs { width:0px; height:0px; overflow:hidden; }

.avisos { color: #444; font-size:10px; }

.twikiToc { padding-top:0px; padding-bottom:0px; background: white; border-top:0px; border-bottom:0px; }

See also the faster WebTopicList

• TWikiGuest - example@your.company

Web Changes Notification Service

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

   * daisy.cutter@flowers.com: Web*

   * TWiki.DaisyCutter: Petal* (1) TWiki.WeedKillers (3) Pretty*Flowers

   * TWiki.StarTrekFan: Star* - *Wars - *sInTheirEyes - *shipTroopers

   * daisy@flowers.com: TWiki.NewsLetter?

   * buttercup@flowers.com: TWiki.NewsLetter! (1)

   * TWiki.GardenGroup: TWiki.AllNewsLetters? (3)
   * petunia@flowers.com: - TWiki.ManureNewsLetter

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

Warning

Can't INCLUDE TWiki.WebSearchAdvanced repeatedly, topic is already included.

Statistics for Research/Rescue Web

Notes:

• Do not edit this topic, it is updated automatically. (You can also force an update)
• TWikiDocumentation tells you how to enable the automatic updates of the statistics.
• Suggestion: You could archive this topic once a year and delete the previous year's statistics from the table.

• RescueDescription
• RescueJobs
• RescueKickOff
• RescueNews
• RescuePartners
• RescuePublications
• RescueTeam
• WebAtom
• WebChanges
• WebCss
• WebHome
• WebIndex
• WebLeftBar
• WebNotify
• WebPreferences
• WebRss
• WebSearch
• WebSearchAdvanced
• WebSideBar
• WebStatistics
• WebTopicCreator
• WebTopicList

See also the verbose WebIndex.