Nikolai Kosmatov

Theor. Comput. Sci., August, 2023

An Efficient Black-Box Support of Advanced Coverage Criteria for Klee.

[BibT_eX]

[DOI]

Proceedings of the 38th ACM/SIGAPP Symposium on Applied Computing, 2023

Towards Formal Verification of a TPM Software Stack.

[BibT_eX]

[DOI]

Proceedings of the iFM 2023 - 18th International Conference, 2023

Execution at RISC: Stealth JOP Attacks on RISC-V Applications.

[BibT_eX]

[DOI]

Proceedings of the Computer Security. ESORICS 2023 International Workshops, 2023

2022

Editorial.

[BibT_eX]

[DOI]

Christophe Gaston

Softw. Qual. J., 2022

Control-Flow Integrity at RISC: Attacking RISC-V by Jump-Oriented Programming.

[BibT_eX]

[DOI]

CoRR, 2022

Verifying redundant-check based countermeasures: a case study.

[BibT_eX]

[DOI]

Thibault Martin

Virgile Prevosto

Proceedings of the SAC '22: The 37th ACM/SIGAPP Symposium on Applied Computing, Virtual Event, April 25, 2022

An Efficient VCGen-Based Modular Verification of Relational Properties.

[BibT_eX]

[DOI]

Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles, 2022

Certified Verification of Relational Properties.

[BibT_eX]

[DOI]

Proceedings of the Integrated Formal Methods - 17th International Conference, 2022

2021

Correction to: PolyGraph: a data flow model with frequency arithmetic.

[BibT_eX]

[DOI]

Int. J. Softw. Tools Technol. Transf., 2021

PolyGraph: a data flow model with frequency arithmetic.

[BibT_eX]

[DOI]

Int. J. Softw. Tools Technol. Transf., 2021

Specify and measure, cover and reveal: A unified framework for automated test generation.

[BibT_eX]

[DOI]

Sci. Comput. Program., 2021

The dogged pursuit of bug-free C programs: the Frama-C software analysis platform.

[BibT_eX]

[DOI]

Commun. ACM, 2021

Runtime Abstract Interpretation for Numerical Accuracy and Robustness.

[BibT_eX]

[DOI]

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2021

Methodology for Specification and Verification of High-Level Requirements with MetAcsl.

[BibT_eX]

[DOI]

Proceedings of the 9th IEEE/ACM International Conference on Formal Methods in Software Engineering, 2021

Formal Verification of a JavaCard Virtual Machine with Frama-C.

[BibT_eX]

[DOI]

Adel Djoudi

Martin Hána

Proceedings of the Formal Methods - 24th International Symposium, 2021

2020

Verified Runtime Assertion Checking for Memory Properties.

[BibT_eX]

[DOI]

Proceedings of the Tests and Proofs - 14th International Conference, 2020

Efficient Runtime Assertion Checking for Properties over Mathematical Numbers.

[BibT_eX]

[DOI]

Fonenantsoa Maurica

Proceedings of the Runtime Verification - 20th International Conference, 2020

Formal Verification of an Industrial Distributed Algorithm: An Experience Report.

[BibT_eX]

[DOI]

Delphine Longuet

Romain Soulat

Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles, 2020

Detection of Polluting Test Objectives for Dataflow Criteria.

[BibT_eX]

[DOI]

Proceedings of the Integrated Formal Methods - 16th International Conference, 2020

2019

Introduction to the STAF 2015 special section.

[BibT_eX]

[DOI]

Softw. Syst. Model., 2019

Abstract Compilation for Verification of Numerical Accuracy Properties.

[BibT_eX]

[DOI]

CoRR, 2019

Tame Your Annotations with MetAcsl: Specifying, Testing and Proving High-Level Properties.

[BibT_eX]

[DOI]

Proceedings of the Tests and Proofs - 13th International Conference, 2019

MetAcsl: Specification and Verification of High-Level Properties.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2019

Logic against ghosts: comparison of two proof approaches for a list module.

[BibT_eX]

[DOI]

Proceedings of the 34th ACM/SIGAPP Symposium on Applied Computing, 2019

Towards Full Proof Automation in Frama-C Using Auto-active Verification.

[BibT_eX]

[DOI]

Proceedings of the NASA Formal Methods - 11th International Symposium, 2019

Dynamic Reconfigurations in Frequency Constrained Data Flow.

[BibT_eX]

[DOI]

Proceedings of the Integrated Formal Methods - 15th International Conference, 2019

A Data Flow Model with Frequency Arithmetic.

[BibT_eX]

[DOI]

Proceedings of the Fundamental Approaches to Software Engineering, 2019

2018

How testing helps to diagnose proof failures.

[BibT_eX]

[DOI]

Formal Aspects Comput., 2018

Cut branches before looking for bugs: certifiably sound verification on relaxed slices.

[BibT_eX]

[DOI]

Formal Aspects Comput., 2018

Self-composition to Prove Relational Properties in Annotated C Program.

[BibT_eX]

[DOI]

CoRR, 2018

MMFilter : A CHR-Based Solver for Generation of Executions under Weak Memory Models.

[BibT_eX]

[DOI]

Comput. Lang. Syst. Struct., 2018

Detection of Security Vulnerabilities in C Code Using Runtime Verification: An Experience Report.

[BibT_eX]

[DOI]

Kostyantyn Vorobyov

Proceedings of the Tests and Proofs - 12th International Conference, 2018

Ghosts for Lists: From Axiomatic to Executable Specifications.

[BibT_eX]

[DOI]

Proceedings of the Tests and Proofs - 12th International Conference, 2018

Static and Dynamic Verification of Relational Properties on Self-composed C Code.

[BibT_eX]

[DOI]

Proceedings of the Tests and Proofs - 12th International Conference, 2018

Tutorial: Secure Your Things: Secure Development of IoT Software with Frama-C.

[BibT_eX]

[DOI]

Proceedings of the 2018 IEEE Cybersecurity Development, SecDev 2018, Cambridge, MA, USA, 2018

Ghosts for Lists: A Critical Module of Contiki Verified in Frama-C.

[BibT_eX]

[DOI]

Proceedings of the NASA Formal Methods - 10th International Symposium, 2018

Test Case Generation with PathCrawler/LTest: How to Automate an Industrial Testing Process.

[BibT_eX]

[DOI]

Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice, 2018

A Lesson on Verification of IoT Software with Frama-C.

[BibT_eX]

[DOI]

Proceedings of the 2018 International Conference on High Performance Computing & Simulation, 2018

Time to clean your test objectives.

[BibT_eX]

[DOI]

Proceedings of the 40th International Conference on Software Engineering, 2018

Fast Computation of Arbitrary Control Dependencies.

[BibT_eX]

[DOI]

Proceedings of the Fundamental Approaches to Software Engineering, 2018

Towards Formal Verification of Contiki: Analysis of the AES-CCM* Modules with Frama-C.

[BibT_eX]

[DOI]

Proceedings of the 2018 International Conference on Embedded Wireless Systems and Networks, 2018

2017

Freeing Testers from Polluting Test Objectives.

[BibT_eX]

[DOI]

CoRR, 2017

From Concurrent Programs to Simulating Sequential Programs: Correctness of a Transformation.

[BibT_eX]

[DOI]

Proceedings of the Proceedings Fifth International Workshop on Verification and Program Transformation, 2017

RPP: Automatic Proof of Relational Properties by Self-composition.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2017

Runtime Detection of Temporal Memory Errors.

[BibT_eX]

[DOI]

Proceedings of the Runtime Verification - 17th International Conference, 2017

E-ACSL, a Runtime Verification Tool for Safety and Security of C Programs (tool paper).

[BibT_eX]

[DOI]

Kostyantyn Vorobyov

Proceedings of the RV-CuBES 2017. An International Workshop on Competitions, 2017

Shadow state encoding for efficient monitoring of block-level properties.

[BibT_eX]

[DOI]

Kostyantyn Vorobyov

Proceedings of the 2017 ACM SIGPLAN International Symposium on Memory Management, 2017

Generic and Effective Specification of Structural Test Objectives.

[BibT_eX]

[DOI]

Proceedings of the 2017 IEEE International Conference on Software Testing, 2017

Taming Coverage Criteria Heterogeneity with LTest.

[BibT_eX]

[DOI]

Proceedings of the 2017 IEEE International Conference on Software Testing, 2017

2016

Fast as a shadow, expressive as a tree: Optimized memory monitoring for C.

[BibT_eX]

[DOI]

Arvid Jakobsson

Sci. Comput. Program., 2016

Deductive Verification with Relational Properties.

[BibT_eX]

[DOI]

CoRR, 2016

Your Proof Fails? Testing Helps to Find the Reason.

[BibT_eX]

[DOI]

Proceedings of the Tests and Proofs - 10th International Conference, 2016

Conc2Seq: A Frama-C Plugin for Verification of Parallel Compositions of C Programs.

[BibT_eX]

[DOI]

Proceedings of the 16th IEEE International Working Conference on Source Code Analysis and Manipulation, 2016

Frama-C, A Collaborative Framework for C Code Verification: Tutorial Synopsis.

[BibT_eX]

[DOI]

Proceedings of the Runtime Verification - 16th International Conference, 2016

A CHR-Based Solver for Weak Memory Behaviors.

[BibT_eX]

[DOI]

Proceedings of the 7th Workshop on Constraint Solvers in Testing, 2016

Static versus Dynamic Verification in Why3, Frama-C and SPARK 2014.

[BibT_eX]

[DOI]

Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques, 2016

Cut Branches Before Looking for Bugs: Sound Verification on Relaxed Slices.

[BibT_eX]

[DOI]

Proceedings of the Fundamental Approaches to Software Engineering, 2016

Formal Verification of a Memory Allocation Module of Contiki with Frama-C: A Case Study.

[BibT_eX]

[DOI]

Frédéric Mangano

Simon Duquennoy

Proceedings of the Risks and Security of Internet and Systems, 2016

2015

Frama-C: A software analysis perspective.

[BibT_eX]

[DOI]

Formal Aspects Comput., 2015

Fast as a shadow, expressive as a tree: hybrid memory monitoring for C.

[BibT_eX]

[DOI]

Arvid Jakobsson

Proceedings of the 30th Annual ACM Symposium on Applied Computing, 2015

Sound and Quasi-Complete Detection of Infeasible Test Requirements.

[BibT_eX]

[DOI]

Proceedings of the 8th IEEE International Conference on Software Testing, 2015

Combining Static and Dynamic Analyses for Vulnerability Detection: Illustration on Heartbleed.

[BibT_eX]

[DOI]

Proceedings of the Hardware and Software: Verification and Testing, 2015

A Case Study on Formal Verification of the Anaxagoros Hypervisor Paging System with Frama-C.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods for Industrial Critical Systems, 2015

2014

Behind the scenes in SANTE: a combination of static and dynamic analyses.

[BibT_eX]

[DOI]

Autom. Softw. Eng., 2014

How Test Generation Helps Software Specification and Deductive Verification in Frama-C.

[BibT_eX]

[DOI]

Proceedings of the Tests and Proofs - 8th International Conference, 2014

Runtime Assertion Checking and Its Combinations with Static and Dynamic Analyses - Tutorial Synopsis.

[BibT_eX]

[DOI]

Proceedings of the Tests and Proofs - 8th International Conference, 2014

A Case Study on Verification of a Cloud Hypervisor by Proof and Structural Testing.

[BibT_eX]

[DOI]

Matthieu Lemerre

Céline Alec

Proceedings of the Tests and Proofs - 8th International Conference, 2014

An All-in-One Toolkit for Automated White-Box Testing.

[BibT_eX]

[DOI]

Proceedings of the Tests and Proofs - 8th International Conference, 2014

Instrumentation of Annotated C Programs for Test Generation.

[BibT_eX]

[DOI]

Proceedings of the 14th IEEE International Working Conference on Source Code Analysis and Manipulation, 2014

Efficient Leveraging of Symbolic Execution to Advanced Coverage Criteria.

[BibT_eX]

[DOI]

Sébastien Bardin

François Cheynier

Proceedings of the Seventh IEEE International Conference on Software Testing, 2014

2013

Efficient Leverage of Symbolic ATG Tools to Advanced Coverage Criteria.

[BibT_eX]

[DOI]

Sébastien Bardin

François Cheynier

CoRR, 2013

A Lesson on Proof of Programs with Frama-C. Invited Tutorial Paper.

[BibT_eX]

[DOI]

Virgile Prevosto

Proceedings of the Tests and Proofs - 7th International Conference, 2013

Structural Unit Testing as a Service with PathCrawler-online.com.

[BibT_eX]

[DOI]

Proceedings of the Seventh IEEE International Symposium on Service-Oriented System Engineering, 2013

Common specification language for static and dynamic analysis of C programs.

[BibT_eX]

[DOI]

Proceedings of the 28th Annual ACM Symposium on Applied Computing, 2013

A Lesson on Runtime Assertion Checking with Frama-C.

[BibT_eX]

[DOI]

Proceedings of the Runtime Verification - 4th International Conference, 2013

An Optimized Memory Monitoring for Runtime Assertion Checking of C Programs.

[BibT_eX]

[DOI]

Guillaume Petiot

Proceedings of the Runtime Verification - 4th International Conference, 2013

A Late Treatment of C Precondition in Dynamic Symbolic Execution Testing Tools.

[BibT_eX]

[DOI]

Proceedings of the Runtime Verification - 4th International Conference, 2013

A Late Treatment of C Precondition in Dynamic Symbolic Execution.

[BibT_eX]

[DOI]

Proceedings of the Sixth IEEE International Conference on Software Testing, 2013

2012

A Lesson on Structural Testing with PathCrawler-online.com.

[BibT_eX]

[DOI]

Proceedings of the Tests and Proofs - 6th International Conference, 2012

Tutorial on Automated Structural Testing with PathCrawler - (Extended Abstract).

[BibT_eX]

[DOI]

Nicky Williams

Proceedings of the Tests and Proofs - 6th International Conference, 2012

Frama-C - A Software Analysis Perspective.

[BibT_eX]

[DOI]

Proceedings of the Software Engineering and Formal Methods - 10th International Conference, 2012

Program slicing enhances a verification technique combining static and dynamic analysis.

[BibT_eX]

[DOI]

Proceedings of the ACM Symposium on Applied Computing, 2012

Structural Testing with PathCrawler: Tutorial Synopsis.

[BibT_eX]

[DOI]

Nicky Williams

Proceedings of the 2012 12th International Conference on Quality Software, 2012

Towards verified cloud computing environments.

[BibT_eX]

[DOI]

Proceedings of the 2012 International Conference on High Performance Computing & Simulation, 2012

2011

The SANTE Tool: Value Analysis, Program Slicing and Test Generation for C Program Debugging.

[BibT_eX]

[DOI]

Proceedings of the Tests and Proofs - 5th International Conference, 2011

Online Test Generation with PathCrawler: Tool Demo.

[BibT_eX]

[DOI]

Proceedings of the Fourth IEEE International Conference on Software Testing, 2011

2010

Combining Static Analysis and Test Generation for C Program Debugging.

[BibT_eX]

[DOI]

Proceedings of the Tests and Proofs - 4th International Conference, 2010

2009

Automating Structural Testing of C Programs: Experience with PathCrawler.

[BibT_eX]

[DOI]

Bernard Botella

Stéphane Hong Tuan Ha

Proceedings of the 4th International Workshop on Automation of Software Test, 2009

2008

All-Paths TestGenerationfor Programs with Internal Aliases.

[BibT_eX]

[DOI]

Proceedings of the 19th International Symposium on Software Reliability Engineering (ISSRE 2008), 2008

2006

A constraint solver for sequences and its applications.

[BibT_eX]

[DOI]

Proceedings of the 2006 ACM Symposium on Applied Computing (SAC), 2006

2005

A uniform deductive approach for parameterized protocol safety.

[BibT_eX]

[DOI]

Jean-François Couchot

Alain Giorgetti

Proceedings of the 20th IEEE/ACM International Conference on Automated Software Engineering (ASE 2005), 2005

Constraint Solving for Sequences in Software Validation and Verification.

[BibT_eX]

[DOI]