Samir Genaim

Daniel Kirchner

Proceedings of the Computer Aided Verification - 35th International Conference, 2023

2022

Artifact of the Paper "Formally Verified EVM Block-Optimizations".

[BibT_eX]

[DOI]

Daniel Kirchner

Dataset, November, 2022

When COSTA Met KeY: Verified Cost Bounds.

[BibT_eX]

[DOI]

Proceedings of the Logic of Software. A Tasting Menu of Formal Methods, 2022

2021

Termination Analysis of Programs with Multiphase Control-Flow.

[BibT_eX]

[DOI]

Jesús J. Doménech

Proceedings of the Proceedings 8th Workshop on Horn Clauses for Verification and Synthesis, 2021

Lower-Bound Synthesis Using Loop Specialization and Max-SMT.

[BibT_eX]

[DOI]

Alicia Merayo

Albert Rubio

Proceedings of the Computer Aided Verification - 33rd International Conference, 2021

2020

A Transformational Approach to Resource Analysis with Typed-norms Inference.

[BibT_eX]

[DOI]

Raúl Gutiérrez

Theory Pract. Log. Program., 2020

2019

Control-Flow Refinement by Partial Evaluation, and its Application to Termination and Cost Analysis.

[BibT_eX]

[DOI]

Jesús J. Doménech

John P. Gallagher

Theory Pract. Log. Program., 2019

Multiphase-Linear Ranking Functions and Their Relation to Recurrent Sets.

[BibT_eX]

[DOI]

Jesús J. Doménech

Proceedings of the Static Analysis - 26th International Symposium, 2019

2017

Rely-Guarantee Termination and Cost Analyses of Loops with Concurrent Interleavings.

[BibT_eX]

[DOI]

J. Autom. Reason., 2017

EasyInterface: A Toolkit for Rapid Development of GUIs for Research Prototype Tools.

[BibT_eX]

[DOI]

Proceedings of the Fundamental Approaches to Software Engineering, 2017

On Multiphase-Linear Ranking Functions.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 29th International Conference, 2017

May-Happen-in-Parallel Analysis with Returned Futures.

[BibT_eX]

[DOI]

Pablo Gordillo

Proceedings of the Automated Technology for Verification and Analysis, 2017

2016

May-Happen-in-Parallel Analysis for Actor-Based Concurrency.

[BibT_eX]

[DOI]

ACM Trans. Comput. Log., 2016

A formal verification framework for static analysis - As well as its instantiation to the resource analyzer COSTA and formal verification tool KeY.

[BibT_eX]

[DOI]

Softw. Syst. Model., 2016

2015

Object-sensitive cost analysis for concurrent objects.

[BibT_eX]

[DOI]

Jesús Correas Fernández

Softw. Test. Verification Reliab., 2015

A practical comparator of cost functions and its applications.

[BibT_eX]

[DOI]

Sci. Comput. Program., 2015

May-Happen-in-Parallel Analysis for Asynchronous Programs with Inter-Procedural Synchronization.

[BibT_eX]

[DOI]

Pablo Gordillo

Proceedings of the Static Analysis - 22nd International Symposium, 2015

Preparing HPC Applications for Exascale: Challenges and Recommendations.

[BibT_eX]

[DOI]

Proceedings of the 18th International Conference on Network-Based Information Systems, 2015

From non-zenoness verification to termination.

[BibT_eX]

[DOI]

Proceedings of the 13. ACM/IEEE International Conference on Formal Methods and Models for Codesign, 2015

May-Happen-in-Parallel Analysis with Condition Synchronization.

[BibT_eX]

[DOI]

Proceedings of the Foundational and Practical Aspects of Resource Analysis, 2015

Resource Analysis: From Sequential to Concurrent and Distributed Programs.

[BibT_eX]

[DOI]

Proceedings of the FM 2015: Formal Methods, 2015

Complexity of Bradley-Manna-Sipma Lexicographic Ranking Functions.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 27th International Conference, 2015

2014

Inference of Field-Sensitive Reachability and Cyclicity.

[BibT_eX]

[DOI]

ACM Trans. Comput. Log., 2014

Conditional termination of loops over heap-allocated data.

[BibT_eX]

[DOI]

Sci. Comput. Program., 2014

Ranking Functions for Linear-Constraint Loops.

[BibT_eX]

[DOI]

J. ACM, 2014

SACO: Static Analyzer for Concurrent Objects.

[BibT_eX]

[DOI]

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

2013

On the Inference of Resource Usage Upper and Lower Bounds.

[BibT_eX]

[DOI]

Abu Naser Masud

ACM Trans. Comput. Log., 2013

Corrigendum to "Reachability-based acyclicity analysis by abstract interpretation" [Theoretical Computer Science 474 (2013) 60-79].

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2013

Reachability-based acyclicity analysis by Abstract Interpretation.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2013

Heap space analysis for garbage collected languages.

[BibT_eX]

[DOI]

Sci. Comput. Program., 2013

Inference of Field-Dependent Cyclicity.

[BibT_eX]

[DOI]

CoRR, 2013

On the linear ranking problem for integer linear-constraint loops.

[BibT_eX]

[DOI]

Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2013

May-Happen-in-Parallel Analysis for Priority-Based Scheduling.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2013

A Transformational Approach to Resource Analysis with Typed-Norms.

[BibT_eX]

[DOI]

Raúl Gutiérrez

Proceedings of the Logic-Based Program Synthesis and Transformation, 2013

May-Happen-in-Parallel Based Deadlock Analysis for Concurrent Objects.

[BibT_eX]

[DOI]

Proceedings of the Formal Techniques for Distributed Systems, 2013

Proving Termination Starting from the End.

[BibT_eX]

[DOI]

Pierre Ganty

Proceedings of the Computer Aided Verification - 25th International Conference, 2013

Precise Cost Analysis via Local Reasoning.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2013

Termination and Cost Analysis of Loops with Concurrent Interleavings.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2013

2012

On the Termination of Integer Loops.

[BibT_eX]

[DOI]

Abu Naser Masud

ACM Trans. Program. Lang. Syst., 2012

Cost analysis of object-oriented bytecode programs.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2012

MayPar: a may-happen-in-parallel analyzer for concurrent objects.

[BibT_eX]

[DOI]

Proceedings of the 20th ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE-20), 2012

On the Limits of the Classical Approach to Cost Analysis.

[BibT_eX]

[DOI]

Proceedings of the Static Analysis - 19th International Symposium, 2012

COSTABS: a cost and termination analyzer for ABS.

[BibT_eX]

[DOI]

Proceedings of the ACM SIGPLAN 2012 Workshop on Partial Evaluation and Program Manipulation, 2012

Automatic Inference of Resource Consumption Bounds.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2012

Analysis of May-Happen-in-Parallel in Concurrent Objects.

[BibT_eX]

[DOI]

Proceedings of the Formal Techniques for Distributed Systems, 2012

Automatic Inference of Bounds on Resource Consumption.

[BibT_eX]

[DOI]

Jesús Correas

Proceedings of the Formal Methods for Components and Objects, 2012

Verified Resource Guarantees for Heap Manipulating Programs.

[BibT_eX]

[DOI]

Proceedings of the Fundamental Approaches to Software Engineering, 2012

2011

Closed-Form Upper Bounds in Static Cost Analysis.

[BibT_eX]

[DOI]

J. Autom. Reason., 2011

Handling Non-linear Operations in the Value Analysis of COSTA.

[BibT_eX]

[DOI]

Proceedings of the Sixth Workshop on Bytecode Semantics, 2011

More Precise Yet Widely Applicable Cost Analysis.

[BibT_eX]

[DOI]

Abu Naser Masud

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

Verified resource guarantees using COSTA and KeY.

[BibT_eX]

[DOI]

Proceedings of the 2011 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, 2011

Task-level analysis for a language with async/finish parallelism.

[BibT_eX]

[DOI]

Proceedings of the ACM SIGPLAN/SIGBED 2011 conference on Languages, 2011

Simulating Concurrent Behaviors with Worst-Case Cost Bounds.

[BibT_eX]

[DOI]

Silvia Lizeth Tapia Tarifa

Einar Broch Johnsen

Rudolf Schlatte

Proceedings of the FM 2011: Formal Methods, 2011

Cost Analysis of Concurrent OO Programs.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems - 9th Asian Symposium, 2011

2010

From Object Fields to Local Variables: A Practical Approach to Field-Sensitive Analysis.

[BibT_eX]

[DOI]

Diana V. Ramírez-Deantes

Proceedings of the Static Analysis - 17th International Symposium, 2010

Parametric inference of memory requirements for garbage collected languages.

[BibT_eX]

[DOI]

Proceedings of the 9th International Symposium on Memory Management, 2010

2009

Preface.

[BibT_eX]

[DOI]

Proceedings of the Fourth Workshop on Bytecode Semantics, 2009

Termination and Cost Analysis with COSTA and its User Interfaces.

[BibT_eX]

[DOI]

Diana V. Ramírez-Deantes

Proceedings of the Ninth Spanish Conference on Programming and Languages, 2009

A declarative encoding of telecommunications feature subscription in SAT.

[BibT_eX]

[DOI]

Peter J. Stuckey

Proceedings of the 11th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 2009

Live heap space analysis for languages with garbage collection.

[BibT_eX]

[DOI]

Proceedings of the 8th International Symposium on Memory Management, 2009

Resource Usage Analysis and Its Application to Resource Certification.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Security Analysis and Design V, 2009

Comparing Cost Functions in Resource Analysis.

[BibT_eX]

[DOI]

Proceedings of the Foundational and Practical Aspects of Resource Analysis, 2009

Field-Sensitive Value Analysis by Field-Insensitive Analysis.

[BibT_eX]

[DOI]

Proceedings of the FM 2009: Formal Methods, 2009

Asymptotic Resource Usage Bounds.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 7th Asian Symposium, 2009

2008

Inferring non-suspension conditions for logic programs with dynamic scheduling.

[BibT_eX]

[DOI]

Andy King

ACM Trans. Comput. Log., 2008

Cost Relation Systems: A Language-Independent Target Language for Cost Analysis.

[BibT_eX]

[DOI]

Proceedings of the Eighth Spanish Conference on Programming and Computer Languages, 2008

Automatic Inference of Upper Bounds for Recurrence Relations in Cost Analysis.

[BibT_eX]

[DOI]

Proceedings of the Static Analysis, 15th International Symposium, 2008

Removing useless variables in cost analysis of Java bytecode.

[BibT_eX]

[DOI]

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

Termination Analysis of Java Bytecode.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods for Open Object-Based Distributed Systems, 2008

2007

Termination analysis of logic programs through combination of type-based norms.

[BibT_eX]

[DOI]

ACM Trans. Program. Lang. Syst., 2007

Experiments in Cost Analysis of Java Bytecode.

[BibT_eX]

[DOI]

Proceedings of the Second Workshop on Bytecode Semantics, 2007

Heap space analysis for java bytecode.

[BibT_eX]

[DOI]

Proceedings of the 6th International Symposium on Memory Management, 2007

COSTA: Design and Implementation of a Cost and Termination Analyzer for Java Bytecode.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods for Components and Objects, 6th International Symposium, 2007

Cost Analysis of Java Bytecode.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 2007

2006

Detecting Determinacy in Prolog Programs.

[BibT_eX]

[DOI]

Andy King

Lunjin Lu

Proceedings of the Logic Programming, 22nd International Conference, 2006

2005

Inferring Termination Conditions for Logic Programs using Backwards Analysis.

[BibT_eX]

[DOI]

Theory Pract. Log. Program., 2005

Information Flow Analysis for Java Bytecode.

[BibT_eX]

[DOI]

Fausto Spoto

Proceedings of the Verification, 2005

2003

Proving Termination One Loop at a Time.

[BibT_eX]

Proceedings of the 13th International Workshop on Logic Programming Environments, 2003

Goal-Independent Suspension Analysis for Logic Programs with Dynamic Scheduling.

[BibT_eX]

[DOI]

Andy King

Proceedings of the Programming Languages and Systems, 2003

2002

Combining Norms to Prove Termination.

[BibT_eX]

[DOI]

Proceedings of the Verification, 2002

Reuse of Results in Termination Analysis of Typed Logic Programs.

[BibT_eX]

[DOI]

Proceedings of the Static Analysis, 9th International Symposium, 2002

2001

Worst-case groundness analysis using definite boolean functions.

[BibT_eX]

[DOI]

Jacob M. Howe

Theory Pract. Log. Program., 2001

Higher-Precision Groundness Analysis.

[BibT_eX]

[DOI]

Proceedings of the Logic Programming, 17th International Conference, 2001

The Def-inite Approach to Dependency Analysis.

[BibT_eX]

[DOI]