2025
Formalization of Android Activity-Fragment Multitasking Mechanism and Static Analysis of Mobile Apps.
Formal Aspects Comput., June, 2025
An efficient string solver for string constraints with regex-counting and string-length.
J. Syst. Archit., 2025
ODE-DSN: A surrogate model for dynamic stiffness in microscopic RVE problems under nonuniform time-step strain inputs.
J. Comput. Des. Eng., 2025
2024
A decision procedure for string constraints with string/integer conversion and flat regular constraints.
Acta Informatica, March, 2024
SAT-based Formal Verification of Fault Injection Countermeasures for Cryptographic Circuits.
IACR Trans. Cryptogr. Hardw. Embed. Syst., 2024
Deciding Separation Logic with Pointer Arithmetic and Inductive Definitions.
CoRR, 2024
Formal Verification of RISC-V Processor Chisel Designs.
Proceedings of the Dependable Software Engineering. Theories, Tools, and Applications, 2024
Compositional Verification of Cryptographic Circuits Against Fault Injection Attacks.
Proceedings of the Formal Methods - 26th International Symposium, 2024
Verifying Randomized Consensus Protocols with Common Coins.
Proceedings of the 54th Annual IEEE/IFIP International Conference on Dependable Systems and Networks, 2024
Formally Verifying Arithmetic Chisel Designs for All Bit Widths at Once.
Proceedings of the 61st ACM/IEEE Design Automation Conference, 2024
2023
SAT-based Formal Fault-Resistance Verification of Cryptographic Circuits.
CoRR, 2023
String Constraints with Regex-Counting and String-Length Solved More Efficiently.
Proceedings of the Dependable Software Engineering. Theories, Tools, and Applications, 2023
2022
Solving string constraints with Regex-dependent functions through transducers with priorities and variables.
Proc. ACM Program. Lang., 2022
CHA: Supporting SVA-Like Assertions in Formal Verification of Chisel Programs (Tool Paper).
Proceedings of the Software Engineering and Formal Methods - 20th International Conference, 2022
2021
Solving Not-Substring Constraint withFlat Abstraction.
Proceedings of the Programming Languages and Systems - 19th Asian Symposium, 2021
2020
Monadic Decomposition in Integer Linear Arithmetic (Technical Report).
CoRR, 2020
Computing Linear Arithmetic Representation of Reachability Relation of One-Counter Automata.
Proceedings of the Dependable Software Engineering. Theories, Tools, and Applications, 2020
Monadic Decomposition in Integer Linear Arithmetic.
Proceedings of the Automated Reasoning - 10th International Joint Conference, 2020
A Decision Procedure for Path Feasibility of String Manipulating Programs with Integer Data Type.
Proceedings of the Automated Technology for Verification and Analysis, 2020
2019
Decision procedures for path feasibility of string-manipulating programs with complex operations.
Proc. ACM Program. Lang., 2019
SL-COMP: Competition of Solvers for Separation Logic.
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2019
Separation Logic with Linearly Compositional Inductive Predicates and Set Data Constraints.
Proceedings of the SOFSEM 2019: Theory and Practice of Computer Science, 2019
Android Multitasking Mechanism: Formal Semantics and Static Analysis of Apps.
Proceedings of the Programming Languages and Systems - 17th Asian Symposium, 2019
2018
What is decidable about string constraints with the ReplaceAll function.
Proc. ACM Program. Lang., 2018
Proceedings of the Computer Aided Verification - 30th International Conference, 2018
2017
The Complexity of SORE-definability Problems.
Proceedings of the 42nd International Symposium on Mathematical Foundations of Computer Science, 2017
Register automata with linear arithmetic.
Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, 2017
Model Checking Pushdown Epistemic Game Structures.
Proceedings of the Formal Methods and Software Engineering, 2017
Tractability of Separation Logic with Inductive Definitions: Beyond Lists.
Proceedings of the 28th International Conference on Concurrency Theory, 2017
Satisfiability of Compositional Separation Logic with Tree Predicates and Data Constraints.
Proceedings of the Automated Deduction - CADE 26, 2017
2016
On temporal logics with data variable quantifications: Decidability and complexity.
Inf. Comput., 2016
Semipositivity in Separation Logic with Two Variables.
Proceedings of the Dependable Software Engineering: Theories, Tools, and Applications, 2016
Formal Reasoning on Infinite Data Values: An Ongoing Quest.
Proceedings of the Engineering Trustworthy Software Systems - Second International School, 2016
Verifying Pushdown Multi-Agent Systems against Strategy Logics.
Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, 2016
The Commutativity Problem of the MapReduce Framework: A Transducer-Based Approach.
Proceedings of the Computer Aided Verification - 28th International Conference, 2016
A Complete Decision Procedure for Linearly Compositional Separation Logic with Data Constraints.
Proceedings of the Automated Reasoning - 8th International Joint Conference, 2016
Global Model Checking on Pushdown Multi-Agent Systems.
Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence, 2016
2015
On the Satisfiability of Indexed Linear Temporal Logics.
Proceedings of the 26th International Conference on Concurrency Theory, 2015
On Automated Lemma Generation for Separation Logic with Inductive Definitions.
Proceedings of the Automated Technology for Verification and Analysis, 2015
2014
On effective construction of the greatest solution of language inequality XA ⊆ BX.
Theor. Comput. Sci., 2014
Regular path queries on graphs with data: A rigid approach.
CoRR, 2014
Extending Temporal Logics with Data Variable Quantifications.
Proceedings of the 34th International Conference on Foundation of Software Technology and Theoretical Computer Science, 2014
2013
Recursive queries on trees and data trees.
Proceedings of the Joint 2013 EDBT/ICDT Conferences, 2013
2012
On Injective Embeddings of Tree Patterns
CoRR, 2012
Commutative Data Automata.
Proceedings of the Computer Science Logic (CSL'12), 2012
2011
A Decidable Extension of Data Automata
Proceedings of Second International Symposium on Games, 2011
2010
Feasibility of motion planning on acyclic and strongly connected directed graphs.
Discret. Appl. Math., 2010
Distributed tree decomposition of graphs and applications to verification.
Proceedings of the 24th IEEE International Symposium on Parallel and Distributed Processing, 2010
Verifying Recursive Active Documents with Positive Data Tree Rewriting.
Proceedings of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2010
2009
On the distributed evaluation of recursive queries over graphs
CoRR, 2009
Logical locality entails frugal distributed computation over graphs
CoRR, 2009
On Distributed Model Checking of MSO on Graphs
CoRR, 2009
Logical Locality Entails Frugal Distributed Computation over Graphs (Extended Abstract).
Proceedings of the Graph-Theoretic Concepts in Computer Science, 2009
Feasibility of Motion Planning on Directed Graphs.
Proceedings of the Theory and Applications of Models of Computation, 6th Annual Conference, 2009
2007
A note on the characterization of TL[EF].
Inf. Process. Lett., 2007
On the Expressive Power of QLTL.
Proceedings of the Theoretical Aspects of Computing, 2007
2005
Quasi-star-free Languages on Infinite Words.
Acta Cybern., 2005
MPEG-4 outer-inner lip FAP interpolation.
Proceedings of the Electronic Imaging: Image and Video Communications and Processing 2005, 2005
2004
A Formal Framework of UML.
Proceedings of the International Conference on Software Engineering Research and Practice, 2004
Inner lip feature extraction for MPEG-4 facial animation.
Proceedings of the 2004 IEEE International Conference on Acoustics, 2004
2002
Audio-Visual Speech Recognition Using MPEG-4 Compliant Visual Features.
EURASIP J. Adv. Signal Process., 2002
Lip Tracking for MPEG-4 Facial Animation.
Proceedings of the 4th IEEE International Conference on Multimodal Interfaces (ICMI 2002), 2002
Audio-visual continuous speech recognition using MPEG-4 compliant visual features.
Proceedings of the 2002 International Conference on Image Processing, 2002