# Panagiotis Manolios

According to our database

Collaborative distances:

^{1}, Panagiotis Manolios authored at least 72 papers between 1994 and 2019.Collaborative distances:

## Timeline

#### Legend:

Book In proceedings Article PhD thesis Other## Links

#### Homepage:

#### On csauthors.net:

## Bibliography

2019

Automating requirements analysis and test case generation.

Requir. Eng., 2019

Records with rank polymorphism.

Proceedings of the 6th ACM SIGPLAN International Workshop on Libraries, 2019

Local and Compositional Reasoning for Optimized Reactive Systems.

Proceedings of the Computer Aided Verification - 31st International Conference, 2019

2018

Checking multi-view consistency of discrete systems with respect to periodic sampling abstractions.

Sci. Comput. Program., 2018

Towards Development of Complete and Conflict-Free Requirements.

Proceedings of the 26th IEEE International Requirements Engineering Conference, 2018

Rank polymorphism viewed as a constraint problem.

Proceedings of the 5th ACM SIGPLAN International Workshop on Libraries, 2018

2015

Proving Skipping Refinement with ACL2s.

Proceedings of the Proceedings Thirteenth International Workshop on the ACL2 Theorem Prover and Its Applications, 2015

Practical Formal Verification of Domain-Specific Language Applications.

Proceedings of the NASA Formal Methods - 7th International Symposium, 2015

The Inez Mathematical Programming Modulo Theories Framework.

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

Skipping Refinement.

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

2014

Data Definitions in the ACL2 Sedan.

Proceedings of the Proceedings Twelfth International Workshop on the ACL2 Theorem Prover and its Applications, 2014

Software for Quantifier Elimination in Propositional Logic.

Proceedings of the Mathematical Software - ICMS 2014, 2014

Partial Quantifier Elimination.

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

ILP Modulo Data.

Proceedings of the Formal Methods in Computer-Aided Design, 2014

An Array-Oriented Language with Static Rank Polymorphism.

Proceedings of the Programming Languages and Systems, 2014

2013

Counterexample Generation Meets Interactive Theorem Proving: Current Results and Future Opportunities.

Proceedings of the Interactive Theorem Proving - 4th International Conference, 2013

Quantifier elimination via clause redundancy.

Proceedings of the Formal Methods in Computer-Aided Design, 2013

ILP Modulo Theories.

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

2012

Quantifier elimination by Dependency Sequents.

Proceedings of the Formal Methods in Computer-Aided Design, 2012

2011

Integrating Testing and Interactive Theorem Proving

Proceedings of the Proceedings 10th International Workshop on the ACL2 Theorem Prover and its Applications, 2011

The ACL2 Sedan Theorem Proving System.

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

Pseudo-Boolean Solving by incremental translation to SAT.

Proceedings of the International Conference on Formal Methods in Computer-Aided Design, 2011

Automated specification analysis using an interactive theorem prover.

Proceedings of the International Conference on Formal Methods in Computer-Aided Design, 2011

Synthesizing Cyber-Physical Architectural Models with Real-Time Constraints.

Proceedings of the Computer Aided Verification - 23rd International Conference, 2011

2010

Generating High-Quality Tests for Boolean Circuits by Treating Tests as Proof Encoding.

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

Interactive Termination Proofs Using Termination Cores.

Proceedings of the Interactive Theorem Proving, First International Conference, 2010

SAT-Solving Based on Boundary Point Elimination.

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

Verifying Pipelines with BAT.

Proceedings of the Design and Verification of Microprocessor Systems for High-Assurance Applications., 2010

2009

A PosterioriSoundness for Non-deterministic Abstract Interpretations.

Proceedings of the Verification, 2009

All-Termination(T).

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

Fast, All-Purpose State Storage.

Proceedings of the Model Checking Software, 2009

Faster SAT solving with better CNF generation.

Proceedings of the Design, Automation and Test in Europe, 2009

2008

A Refinement-Based Compositional Reasoning Framework for Pipelined Machine Verification.

IEEE Trans. VLSI Syst., 2008

WASP: Protecting Web Applications Using Positive Tainting and Syntax-Aware Evaluation.

IEEE Trans. Software Eng., 2008

Automatic verification of safety and liveness for pipelined machines using WEB refinement.

ACM Trans. Design Autom. Electr. Syst., 2008

Efficient execution in an automated reasoning environment.

J. Funct. Program., 2008

2007

Checking Pedigree Consistency with PCS.

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

Efficient Circuit to CNF Conversion.

Proceedings of the Theory and Applications of Satisfiability Testing, 2007

Automating component-based system assembly.

Proceedings of the ACM/SIGSOFT International Symposium on Software Testing and Analysis, 2007

ACL2s: "The ACL2 Sedan".

Proceedings of the 29th International Conference on Software Engineering (ICSE 2007), 2007

BAT: The Bit-Level Analysis Tool.

Proceedings of the Computer Aided Verification, 19th International Conference, 2007

2006

A Framework for Verifying Bit-Level Pipelined Machines Based on Automated Deduction and Decision Procedures.

J. Autom. Reasoning, 2006

Using positive tainting and syntax-aware evaluation to counter SQL injection attacks.

Proceedings of the 14th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2006

Refinement and Theorem Proving.

Proceedings of the Formal Methods for Hardware Verification, 2006

Implementing Survey Propagation on Graphics Processing Units.

Proceedings of the Theory and Applications of Satisfiability Testing, 2006

Integrating static analysis and general-purpose theorem proving for termination analysis.

Proceedings of the 28th International Conference on Software Engineering (ICSE 2006), 2006

Automatic memory reductions for RTL model verification.

Proceedings of the 2006 International Conference on Computer-Aided Design, 2006

Monolithic verification of deep pipelines with collapsed flushing.

Proceedings of the Conference on Design, Automation and Test in Europe, 2006

Termination Analysis with Calling Context Graphs.

Proceedings of the Computer Aided Verification, 18th International Conference, 2006

2005

Ordinal Arithmetic: Algorithms and Mechanization.

J. Autom. Reasoning, 2005

The Challenge of Hardware-Software Co-verification.

Proceedings of the Verified Software: Theories, 2005

Enhanced Probabilistic Verification with 3Spin and 3Murphi.

Proceedings of the Model Checking Software, 2005

A computationally ef~cient method based on commitment re~nement maps for verifying pipelined machines.

Proceedings of the 3rd ACM & IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE 2005), 2005

A complete compositional reasoning framework for the efficient verification of pipelined machines.

Proceedings of the 2005 International Conference on Computer-Aided Design, 2005

Verification of executable pipelined machines with bit-level interfaces.

Proceedings of the 2005 International Conference on Computer-Aided Design, 2005

Refinement Maps for Efficient Verification of Processor Models.

Proceedings of the 2005 Design, 2005

A Parameterized Benchmark Suite of Hard Pipelined-Machine-Verification Problems.

Proceedings of the Correct Hardware Design and Verification Methods, 2005

2004

Fast and Accurate Bitstate Verification for SPIN.

Proceedings of the Model Checking Software, 2004

Integrating Reasoning About Ordinal Arithmetic into ACL2.

Proceedings of the Formal Methods in Computer-Aided Design, 5th International Conference, 2004

Bloom Filters in Probabilistic Verification.

Proceedings of the Formal Methods in Computer-Aided Design, 5th International Conference, 2004

Automatic Verification of Safety and Liveness for XScale-Like Processor Models Using WEB Refinements.

Proceedings of the 2004 Design, 2004

2003

Partial Functions in ACL2.

J. Autom. Reasoning, 2003

A lattice-theoretic characterization of safety and liveness.

Proceedings of the Twenty-Second ACM Symposium on Principles of Distributed Computing, 2003

Brief announcement: branching time refinement.

Proceedings of the Twenty-Second ACM Symposium on Principles of Distributed Computing, 2003

A Compositional Theory of Refinement for Branching Time.

Proceedings of the Correct Hardware Design and Verification Methods, 2003

Algorithms for Ordinal Arithmetic.

Proceedings of the Automated Deduction - CADE-19, 19th International Conference on Automated Deduction Miami Beach, FL, USA, July 28, 2003

2001

On the desirability of mechanizing calculational proofs.

Inf. Process. Lett., 2001

Safety and Liveness in Branching Time.

Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, 2001

2000

Correctness of Pipelined Machines.

Proceedings of the Formal Methods in Computer-Aided Design, Third International Conference, 2000

1999

Model Checking TLA

^{+}Specifications.
Proceedings of the Correct Hardware Design and Verification Methods, 1999

Linking Theorem Proving and Model-Checking with Well-Founded Bisimulation.

Proceedings of the Computer Aided Verification, 11th International Conference, 1999

1994

First-Order Recurrent Neural Networks and Deterministic Finite State Automata.

Neural Computation, 1994