Fetching the paper…
Reading the bibliography…
Symbolic execution is a classical program analysis technique used to show that programs satisfy or violate given specifications.
A Basis for a Mathematical Theory of Computation (preliminary report). In Proceedings of the Western Joint Computer Conference , Cicely M. Popplewell (Ed.). IRE, AIEE, ACM, 225–238
John McCarthy. 1961 · 1961
Earlier work this paper cites.
Symbolic Execution and Program Testing
James C. King. 1976 · 1976
Earlier work this paper cites.
Security Policies and Security Models. In 1982 IEEE Symposium on Security and Privacy, Oakland, CA, USA, April 26-28, 1982 . 11–20
Joseph A. Goguen and José Meseguer. 1982 · 1982
Earlier work this paper cites.
Unwinding and Inference Control. In Proceedings of the 1984 IEEE Symposium on Security and Privacy, Oakland, California, USA, April 29 - May 2, 1984 . 75–87
Joseph A. Goguen and José Meseguer. 1984 · 1984
Earlier work this paper cites.
A Sound Type System for Secure Flow Analysis
Dennis M. Volpano, Cynthia E. Irvine, and Geoffrey Smith. 1996 · 1996
Earlier work this paper cites.
Abstract Interpretation-Based Static Analysis of Mobile Ambients. In Eighth International Static Analysis Symposium (SAS’01) (LNCS) . Springer-Verlag
Jérôme Feret. 2001 · 2001
Earlier work this paper cites.
Generalized Symbolic Execution for Model Checking and Testing. In Proceedings of the 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’03) . 553–568
Sarfraz Khurshid, Corina S. Păsăreanu, and Willem Visser. 2003 · 2003
Earlier work this paper cites.
Information Flow Inference for ML
François Pottier and Vincent Simonet. 2003 · 2003
Earlier work this paper cites.
Secure Information Flow by Self-Composition. In Proceedings of the 17th IEEE Workshop on Computer Security Foundations (CSFW ’04)
Gilles Barthe, Pedro R. D’Argenio, and Tamara Rezk. 2004 · 2004
Earlier work this paper cites.
Simple Relational Correctness Proofs for Static Analyses and Program Transformations. In Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’04) . ACM, New York, NY, USA, 14–25
Nick Benton. 2004 · 2004
Earlier work this paper cites.
Abstract non-interference: parameterizing non-interference by abstract interpretation. In Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2004, Venice, Italy, January 14-16, 2004 . 186–197
Roberto Giacobazzi and Isabella Mastroeni. 2004 · 2004
Earlier work this paper cites.
A Theorem Proving Approach to Analysis of Secure Information Flow. In Proceedings of the Second International Conference on Security in Pervasive Computing (SPC’05) . Springer-Verlag, Berlin, Heidelberg, 193–209
Ádám Darvas, Reiner Hähnle, and David Sands. 2005 · 2005
Earlier work this paper cites.
Secure Information Flow As a Safety Problem. In Proceedings of the 12th International Conference on Static Analysis (SAS’05) . 352–367
Tachio Terauchi and Alex Aiken. 2005 · 2005
Earlier work this paper cites.
Z3: An Efficient SMT Solver. In Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’08/ETAPS’08) . 337–340
Leonardo De Moura and Nikolaj Bjørner. 2008 · 2008
Earlier work this paper cites.
Elimination of Ghost Variables in Program Logics. In Trustworthy Global Computing . Springer Berlin Heidelberg, Berlin, Heidelberg
Martin Hofmann and Mariela Pavlova. 2008 · 2008
Earlier work this paper cites.
Differential Symbolic Execution. In Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of Software Engineering (SIGSOFT ’08/FSE-16) . 226–237
Suzette Person, Matthew B. Dwyer, Sebastian Elbaum, and Corina S. Pǎsǎreanu. 2008 · 2008
Earlier work this paper cites.
Continuity Analysis of Programs. In Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’10) . ACM, New York, NY, USA, 57–70
Swarat Chaudhuri, Sumit Gulwani, and Roberto Lublinerman. 2010 · 2010
Earlier work this paper cites.
Distance makes the types grow stronger: a calculus for differential privacy. In Proceeding of the 15th ACM SIGPLAN international conference on Functional programming, ICFP 2010, Baltimore, Maryland, USA, September 27-29, 2010 . 157–168
Jason Reed and Benjamin C. Pierce. 2010 · 2010
Cited alongside, same era.
Relational Verification Using Product Programs. In Proceedings of the 17th International Conference on Formal Methods (FM’11) . Springer-Verlag, Berlin, Heidelberg, 200–214
Gilles Barthe, Juan Manuel Crespo, and César Kunz. 2011 · 2011
Cited alongside, same era.
Relational Decomposition. In Interactive Theorem Proving . Springer Berlin Heidelberg, Berlin, Heidelberg, 39–54
Lennart Beringer. 2011 · 2011
Cited alongside, same era.
FM 2011: Formal Methods - 17th International Symposium on Formal Methods, Limerick, Ireland, June 20-24, 2011. Proceedings . Lecture Notes in Computer Science, Vol. 6664. Springer
Michael J. Butler and Wolfram Schulte (Eds.). 2011 · 2011
Cited alongside, same era.
Probabilistic Relational Verification for Cryptographic Implementations
Gilles Barthe, Cédric Fournet, Benjamin Grégoire, Pierre-Yves Strub, Nikhil Swamy, and Santiago Zanella-Béguelin. 2014b · 2014
Later among the works it cites.
A Separation Logic for Enforcing Declarative Information Flow Control Policies. In Principles of Security and Trust - Third International Conference, POST 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings . 179–198
David Costanzo and Zhong Shao. 2014 · 2014
Later among the works it cites.
Symbolic Execution Debugger (SED). In Proceedings of Runtime Verification 2014 (2014-01-01) (LNCS) , Borzoo Bonakdarpour and Scott A. Smolka (Eds.). Springer, 255–262
Martin Hentschel, Richard Bubel, and Reiner Hähnle. 2014 · 2014
Later among the works it cites.
Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015 . 55–68
alphaXiv searches the wider corpus for related work and actual follow-ups.
alphaXiv is searching for related work…
An Iterative Method for Generating Loop Invariants. In Proceedings of the 5th Joint International Frontiers in Algorithmics, and 7th International Conference on Algorithmic Aspects in Information and Management (FAW-AAIM’11)
Shikun Chen, Zhoujun Li, Xiaoyu Song, and Mengjun Li. 2011 · 2011
Cited alongside, same era.
Invariant Generation in Vampire. In Tools and Algorithms for the Construction and Analysis of Systems - 17th International Conference, TACAS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26-April 3, 2011. Proceedings . 60–64
Krystof Hoder, Laura Kovács, and Andrei Voronkov. 2011 · 2011
Cited alongside, same era.
Multiple Facets for Dynamic Information Flow. In Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’12) . ACM, New York, NY, USA, 165–178
Thomas H. Austin and Cormac Flanagan. 2012 · 2012
Cited alongside, same era.
Probabilistic relational reasoning for differential privacy
Gilles Barthe, Boris Köpf, Federico Olmedo, and Santiago Zanella Béguelin. 2012 · 2012
Cited alongside, same era.
Continuity and Robustness of Programs
Swarat Chaudhuri, Sumit Gulwani, and Roberto Lublinerman. 2012 · 2012
Cited alongside, same era.
Noninterference via Symbolic Execution. In Proceedings of the IFIP WG 6.1 International Conference on Formal Techniques for Distributed Systems (FMOODS’12/FORTE’12) . 152–168
Dimiter Milushev, Wim Beck, and Dave Clarke. 2012 · 2012
Cited alongside, same era.
Evaluating the Design of the R Language - Objects and Functions for Data Analysis. In ECOOP 2012 - Object-Oriented Programming - 26th European Conference, Beijing, China, June 11-16, 2012. Proceedings . 104–131
Floréal Morandat, Brandon Hill, Leo Osvald, and Jan Vitek. 2012 · 2012
Cited alongside, same era.
Testing Noninterference, Quickly. In Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming (ICFP ’13) . 455–468
Catalin Hritcu, John Hughes, Benjamin C. Pierce, Antal Spector-Zabusky, Dimitrios Vytiniotis, Arthur Azevedo de Amorim, and Leonidas Lampropoulos. 2013 · 2013
Cited alongside, same era.
Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, Aaron Roth, and Pierre-Yves Strub. 2015 · 2015
Later among the works it cites.
Relational Logic with Framing and Hypotheses. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2016, December 13-15, 2016, Chennai, India . 11:1–11:16
Anindya Banerjee, David A. Naumann, and Mohammad Nikouei. 2016 · 2016
Later among the works it cites.
Cartesian Hoare Logic for Verifying K-safety Properties. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’16) . 57–69
Marcelo Sousa and Isil Dillig. 2016 · 2016
Later among the works it cites.
Decomposition Instead of Self-composition for Proving the Absence of Timing Channels. In Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2017) . ACM, New York, NY, USA, 362–375
Timos Antonopoulos, Paul Gazzillo, Michael Hicks, Eric Koskinen, Tachio Terauchi, and Shiyi Wei. 2017 · 2017
Closest in time.
Verifying Relational Properties of Functional Programs by First-order Refinement
Kazuyuki Asada, Ryosuke Sato, and Naoki Kobayashi. 2017 · 2017
Closest in time.
Hypercollecting semantics and its application to static analysis of information flow. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017 . 874–887
Mounir Assaf, David A. Naumann, Julien Signoles, Eric Totel, and Frédéric Tronel. 2017 · 2017
Closest in time.
Precise Detection of Side-Channel Vulnerabilities using Quantitative Cartesian Hoare Logic. In Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS 2017, Dallas, TX, USA, October 30 - November 03, 2017 . 875–890
Jia Chen, Yu Feng, and Isil Dillig. 2017 · 2017
Closest in time.
Relational cost analysis. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017 . 316–329
Ezgi Çiçek, Gilles Barthe, Marco Gaboardi, Deepak Garg, and Jan Hoffmann. 2017 · 2017
Closest in time.
Proving Flow Security of Sequential Logic via Automatically-Synthesized Relational Invariants. In 30th IEEE Computer Security Foundations Symposium, CSF 2017, Santa Barbara, CA, USA, August 21-25, 2017 . 420–435
Hyoukjun Kwon, William Harris, and Hadi Esmaeilzadeh. 2017 · 2017
Closest in time.
Synthesizing coupling proofs of differential privacy
Aws Albarghouthi and Justin Hsu. 2018 · 2018
Closest in time.
Modular Product Programs. In Programming Languages and Systems , Amal Ahmed (Ed.). Springer International Publishing, Cham, 502–529
Marco Eilers, Peter Müller, and Samuel Hitz. 2018 · 2018
Closest in time.
Exploiting Synchrony and Symmetry in Relational Verification. In Computer Aided Verification
Lauren Pick, Grigory Fedyukovich, and Aarti Gupta. 2018 · 2018
Closest in time.
Nickel: A Framework for Design and Verification of Information Flow Control Systems. In 13th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2018, Carlsbad, CA, USA, October 8-10, 2018
Helgi Sigurbjarnarson, Luke Nelson, Bruno Castro-Karney, James Bornholt, Emina Torlak, and Xi Wang. 2018 · 2018
Closest in time.