BibSLEIGH
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
Travelled to:
1 × Austria
1 × Germany
1 × Hungary
1 × Italy
1 × Japan
1 × Spain
2 × Estonia
2 × France
3 × United Kingdom
4 × USA
Collaborated with:
∅ H.Unno A.Aiken H.Yasuoka E.Koskinen N.Kobayashi J.S.Foster H.U.0001 A.Megacz A.Aiken Y.Satake T.Kuwahara J.Kodumal Akihiro Murase N.K.0001 R.Sato T.Antonopoulos P.Gazzillo M.H.0001 S.Wei
Talks about:
program (8) verif (6) higher (5) order (5) function (4) type (4) complet (3) refin (3) infer (3) flow (3)

Person: Tachio Terauchi

DBLP DBLP: Terauchi:Tachio

Contributed to:

ESOP 20152015
SAS 20152015
TACAS 20152015
ESOP 20142014
CSL-LICS 20142014
POPL 20132013
FLOPS 20122012
QAPL 20122012
POPL 20102010
SAS 20092009
ESOP 20082008
PLDI 20082008
LICS 20062006
ICFP 20052005
SAS 20052005
PLDI 20032003
PLDI 20022002
POPL 20162016
PLDI 20172017
POPL 20182018

Wrote 20 papers:

ESOP-2015-TerauchiU #approach #refinement
Relaxed Stratification: A New Approach to Practical Complete Predicate Refinement (TT, HU), pp. 610–633.
SAS-2015-Terauchi #effectiveness #heuristic #refinement #verification
Explaining the Effectiveness of Small Refinement Heuristics in Program Verification with CEGAR (TT), pp. 128–144.
TACAS-2015-UnnoT #horn clause #recursion
Inferring Simple Solutions to Recursion-Free Horn Clauses via Sampling (HU, TT), pp. 149–163.
ESOP-2014-KuwaharaTU0 #automation #functional #higher-order #source code #termination #verification
Automatic Termination Verification for Higher-Order Functional Programs (TK, TT, HU, NK), pp. 392–411.
LICS-CSL-2014-KoskinenT #reasoning
Local temporal reasoning (EK, TT), p. 10.
POPL-2013-UnnoTK #automation #functional #higher-order #source code #verification
Automating relatively complete verification of higher-order functional programs (HU, TT, NK), pp. 75–86.
FLOPS-2012-Terauchi #automation #functional #higher-order #source code #verification
Automated Verification of Higher-Order Functional Programs (TT), p. 2.
QAPL-2012-YasuokaT #data flow #liveness #safety
Quantitative Information Flow as Safety and Liveness Hyperproperties (HY, TT), pp. 77–91.
POPL-2010-Terauchi #dependent type
Dependent types from counterexamples (TT), pp. 119–130.
SAS-2009-YasuokaT #polymorphism
Polymorphic Fractional Capabilities (HY, TT), pp. 36–51.
ESOP-2008-TerauchiM #bound #linear #programming
Inferring Channel Buffer Bounds Via Linear Programming (TT, AM), pp. 284–298.
PLDI-2008-Terauchi #linear #programming
Checking race freedom via linear programming (TT), pp. 1–10.
LICS-2006-TerauchiA #on the #polymorphism #recursion
On Typability for Rank-2 Intersection Types with Polymorphic Recursion (TT, AA), pp. 111–122.
ICFP-2005-TerauchiA
Witnessing side-effects (TT, AA), pp. 105–115.
SAS-2005-TerauchiA #data flow #problem #safety
Secure Information Flow as a Safety Problem (TT, AA), pp. 352–367.
PLDI-2003-AikenFKT #alias
Checking and inferring local non-aliasing (AA, JSF, JK, TT), pp. 129–140.
PLDI-2002-FosterTA
Flow-Sensitive Type Qualifiers (JSF, TT, AA), pp. 1–12.
POPL-2016-MuraseT0SU #functional #higher-order #source code #verification
Temporal verification of higher-order functional programs (AM, TT, NK0, RS, HU0), pp. 57–68.
PLDI-2017-AntonopoulosGHK #composition #proving #self
Decomposition instead of self-composition for proving the absence of timing channels (TA, PG, MH0, EK, TT, SW), pp. 362–375.
POPL-2018-0001ST #higher-order #nondeterminism #refinement #source code #type system #verification
Relatively complete refinement type system for verification of higher-order non-deterministic programs (HU0, YS, TT), p. 29.
Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.