6 citations · 9 across the 12 of their papers we have counts for
14 papers
Loop-Based Slicing and Input-Driven Concretization: An Empirical Study of Termination and Non-Termination Analysis
Negar Fathi, Rahul Purandare, Tachio Terauchi +1
Termination and non-termination are fundamental correctness properties, but verifying them in real-world C programs remains difficult because loop interactions and nondeterministic…
Hardness of Regular Expression Matching with Extensions
Taisei Nogami, Yoshiki Nakamura, Tachio Terauchi
Regular expression matching asks whether a given regular expression of length matches a given string of length , and its time complexity is fairly well understood. Meanwhile…
Reachability is Decidable for ATM-Typable Finitary PCF with Effect Handlers
Ryunosuke Endo, Tachio Terauchi
It is well known that the reachability problem for simply-typed lambda calculus with recursive definitions and finite base-type values (finitary PCF) is decidable. A recent paper b…
Efficient Matching of Some Fundamental Regular Expressions with Backreferences
Taisei Nogami, Tachio Terauchi
Regular expression matching is of practical importance due to its widespread use in real-world applications. In practical use, regular expressions are often used with real-world ex…
Regular Expressions with Backreferences on Multiple Context-Free Languages, and the Closed-Star Condition
Taisei Nogami, Tachio Terauchi
Backreference is a well-known practical extension of regular expressions and is supported by the regular expression engines in the standard libraries of most modern programming lan…
On the Expressive Power of Regular Expressions with Backreferences
Taisei Nogami, Tachio Terauchi
A rewb is a regular expression extended with a feature called backreference. It is broadly known that backreference is a practical extension of regular expressions, and is supporte…
Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers
Fuga Kawamata, Hiroshi Unno, Taro Sekiyama +1
Algebraic effects and handlers are a mechanism to structure programs with computational effects in a modular way. They are recently gaining popularity and being adopted in practica…
Constraint-based Relational Verification
Hiroshi Unno, Tachio Terauchi, Eric Koskinen
In recent years they have been numerous works that aim to automate relational verification. Meanwhile, although Constrained Horn Clauses (CHCs) empower a wide range of verification…
Repairing DoS Vulnerability of Real-World Regexes
Nariyoshi Chida, Tachio Terauchi
There has been much work on synthesizing and repairing regular expressions (regexes for short) from examples. These programming-by-example (PBE) methods help the users write regexe…
Program Verification via Predicate Constraint Satisfiability Modulo Theories
Hiroshi Unno, Yuki Satake, Tachio Terauchi +1
This paper presents a verification framework based on a new class of predicate Constraint Satisfaction Problems called pCSP where constraints are represented as clauses modulo firs…
Compositional Synthesis of Leakage Resilient Programs
Arthur Blot, Masaki Yamamoto, Tachio Terauchi
A promising approach to defend against side channel attacks is to build programs that are leakage resilient, in a formal sense. One such formal notion of leakage resilience is the…
Quantitative Information Flow as Safety and Liveness Hyperproperties
Hirotoshi Yasuoka, Tachio Terauchi
We employ Clarkson and Schneider's "hyperproperties" to classify various verification problems of quantitative information flow. The results of this paper unify and extend the prev…
On Bounding Problems of Quantitative Information Flow
Hirotoshi Yasuoka, Tachio Terauchi
Researchers have proposed formal definitions of quantitative information flow based on information theoretic notions such as the Shannon entropy, the min entropy, the guessing entr…
Quantitative Information Flow - Verification Hardness and Possibilities
Hirotoshi Yasuoka, Tachio Terauchi
Researchers have proposed formal definitions of quantitative information flow based on information theoretic notions such as the Shannon entropy, the min entropy, the guessing entr…