Aarti Gupta

Affiliations:
  • Princeton University, NJ, USA
  • NEC Labs America, USA (former)


According to our database1, Aarti Gupta authored at least 172 papers between 1986 and 2023.

Collaborative distances:
  • Dijkstra number2 of four.
  • Erdős number3 of four.

Awards

ACM Fellow

ACM Fellow 2017, "For contributions to system analysis and verification techniques and their transfer to industrial practice".

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2023
SoC Protocol Implementation Verification Using Instruction-Level Abstraction Specifications.
ACM Trans. Design Autom. Electr. Syst., November, 2023

Synthesizing MILP Constraints for Efficient and Robust Optimization.
Proc. ACM Program. Lang., 2023

Modular Control Plane Verification via Temporal Invariants.
Proc. ACM Program. Lang., 2023

Psym: Efficient Symbolic Exploration of Distributed Systems.
Proc. ACM Program. Lang., 2023

Combined Scheduling, Memory Allocation and Tensor Replacement for Minimizing Off-Chip Data Accesses of DNN Accelerators.
CoRR, 2023

Towards Integrating Formal Methods into ML-Based Systems for Networking.
Proceedings of the 22nd ACM Workshop on Hot Topics in Networks, 2023

INVITED: Generalizing the ISA to the ILA: A Software/Hardware Interface for Accelerator-rich Platforms.
Proceedings of the 60th ACM/IEEE Design Automation Conference, 2023

CaT: A Solver-Aided Compiler for Packet-Processing Pipelines.
Proceedings of the 28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, 2023

2022
High-Level Synthesis for Packet-Processing Pipelines.
CoRR, 2022

Specialized Accelerators and Compiler Flows: Replacing Accelerator APIs with a Formal Software/Hardware Interface.
CoRR, 2022

Katra: Realtime Verification for Multilayer Networks.
Proceedings of the 19th USENIX Symposium on Networked Systems Design and Implementation, 2022

Kirigami, the Verifiable Art of Network Cutting.
Proceedings of the 30th IEEE International Conference on Network Protocols, 2022

Compositional Verification Using a Formal Component and Interface Specification.
Proceedings of the 41st IEEE/ACM International Conference on Computer-Aided Design, 2022

Usage-Based RTL Subsetting for Hardware Accelerators.
Proceedings of the 41st IEEE/ACM International Conference on Computer-Aided Design, 2022

ACORN: Network Control Plane Abstraction using Route Nondeterminism.
Proceedings of the 22nd Formal Methods in Computer-Aided Design, 2022

Error Correction Code Algorithm and Implementation Verification Using Symbolic Representations.
Proceedings of the 22nd Formal Methods in Computer-Aided Design, 2022

Automatic Generation of Architecture-Level Models from RTL Designs for Processors and Accelerators.
Proceedings of the 2022 Design, Automation & Test in Europe Conference & Exhibition, 2022

Generalizing Tandem Simulation: Connecting High-level and RTL Simulation Models.
Proceedings of the 27th Asia and South Pacific Design Automation Conference, 2022

2021
Syntax-Guided Synthesis for Lemma Generation in Hardware Model Checking.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2021

Unbounded Procedure Summaries from Bounded Environments.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2021

Generating Architecture-Level Abstractions from RTL Designs for Processors and Accelerators Part I: Determining Architectural State Variables.
Proceedings of the IEEE/ACM International Conference On Computer Aided Design, 2021

Leveraging Processor Modeling and Verification for General Hardware Modules.
Proceedings of the Design, Automation & Test in Europe Conference & Exhibition, 2021

Pono: A Flexible and Extensible SMT-Based Model Checker.
Proceedings of the Computer Aided Verification - 33rd International Conference, 2021

2020
Abstract interpretation of distributed network control planes.
Proc. ACM Program. Lang., 2020

Synthesizing Environment Invariants for Modular Hardware Verification.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2020

Fold/Unfold Transformations for Fixpoint Logic.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2020

Switch Code Generation Using Program Synthesis.
Proceedings of the SIGCOMM '20: Proceedings of the 2020 Annual conference of the ACM Special Interest Group on Data Communication on the applications, 2020

In Search for a SAT-friendly Binarized Neural Network Architecture.
Proceedings of the 8th International Conference on Learning Representations, 2020

Automating Modular Verification of Secure Information Flow.
Proceedings of the 2020 Formal Methods in Computer Aided Design, 2020

Verification of Recurrent Neural Networks for Cognitive Tasks via Reachability Analysis.
Proceedings of the ECAI 2020 - 24th European Conference on Artificial Intelligence, 29 August-8 September 2020, Santiago de Compostela, Spain, August 29 - September 8, 2020, 2020

2019
Instruction-Level Abstraction (ILA): A Uniform Specification for System-on-Chip (SoC) Verification.
ACM Trans. Design Autom. Electr. Syst., 2019

Lazy but Effective Functional Synthesis.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2019

ILAng: A Modeling and Verification Platform for SoCs Using Instruction-Level Abstractions.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2019

FlyMC: Highly Scalable Testing of Complex Interleavings in Distributed Systems.
Proceedings of the Fourteenth EuroSys Conference 2019, Dresden, Germany, March 25-28, 2019, 2019

Lemma Synthesis for Automating Induction over Algebraic Data Types.
Proceedings of the Principles and Practice of Constraint Programming, 2019

Functional Synthesis with Examples.
Proceedings of the Principles and Practice of Constraint Programming, 2019

Quantified Invariants via Syntax-Guided Synthesis.
Proceedings of the Computer Aided Verification - 31st International Conference, 2019

2018
Model Checking Concurrent Programs.
Proceedings of the Handbook of Model Checking., 2018

Template-Based Parameterized Synthesis of Uniform Instruction-Level Abstractions for SoC Verification.
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2018

Control plane compression.
Proceedings of the 2018 Conference of the ACM Special Interest Group on Data Communication, 2018

PipeProof: Automated Memory Consistency Proofs for Microarchitectural Specifications.
Proceedings of the 51st Annual IEEE/ACM International Symposium on Microarchitecture, 2018

A formal instruction-level GPU model for scalable verification.
Proceedings of the International Conference on Computer-Aided Design, 2018

ILA-MCM: Integrating Memory Consistency Models with Instruction-Level Abstractions for Heterogeneous System-on-Chip Verification.
Proceedings of the 2018 Formal Methods in Computer Aided Design, 2018

Solving Constrained Horn Clauses Using Syntax and Data.
Proceedings of the 2018 Formal Methods in Computer Aided Design, 2018

Formal security verification of concurrent firmware in SoCs using instruction-level abstraction for hardware.
Proceedings of the 55th Annual Design Automation Conference, 2018

Lazy Self-composition for Security Verification.
Proceedings of the Computer Aided Verification - 30th International Conference, 2018

Exploiting Synchrony and Symmetry in Relational Verification.
Proceedings of the Computer Aided Verification - 30th International Conference, 2018

Syntax-Guided Termination Analysis.
Proceedings of the Computer Aided Verification - 30th International Conference, 2018

2017
A General Approach to Network Configuration Verification.
Proceedings of the Conference of the ACM Special Interest Group on Data Communication, 2017

Trace-based Analysis of Memory Corruption Malware Attacks.
Proceedings of the Hardware and Software: Verification and Testing, 2017

2016
Parallel data race detection for task parallel programs with locks.
Proceedings of the 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2016

Alive-FP: Automated Verification of Floating Point Based Peephole Optimizations in LLVM.
Proceedings of the Static Analysis - 23rd International Symposium, 2016

2015
Scalable and scope-bounded software verification in Varvel.
Autom. Softw. Eng., 2015

Assertion guided symbolic execution of multithreaded programs.
Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering, 2015

Completeness bounds and sequentialization for model checking of interacting firmware and hardware.
Proceedings of the 2015 International Conference on Hardware/Software Codesign and System Synthesis, 2015

2014
RTL2RTL Formal Equivalence: Boosting the Design Confidence.
Proceedings of the Proceedings 2nd French Singaporean Workshop on Formal Methods and Applications, 2014

Environment-Sensitive Performance Tuning for Distributed Service Orchestration.
Proceedings of the High Performance Computing for Computational Science - VECPAR 2014 - 11th International Conference, Eugene, OR, USA, June 30, 2014

Generating consistent updates for software-defined network configurations.
Proceedings of the third workshop on Hot topics in software defined networking, 2014

ARC++: effective typestate and lifetime dependency analysis.
Proceedings of the International Symposium on Software Testing and Analysis, 2014

Formally Verifying Graphics FPU - An Intel® Experience.
Proceedings of the FM 2014: Formal Methods, 2014

An Adaptable Rule Placement for Software-Defined Networks.
Proceedings of the 44th Annual IEEE/IFIP International Conference on Dependable Systems and Networks, 2014

ReproLite: A Lightweight Tool to Quickly Reproduce Hard System Bugs.
Proceedings of the ACM Symposium on Cloud Computing, 2014

2013
Probabilistic Temporal Logic Falsification of Cyber-Physical Systems.
ACM Trans. Embed. Comput. Syst., 2013

Static analysis for concurrent programs with applications to data race detection.
Int. J. Softw. Tools Technol. Transf., 2013

SETSUDŌ: perturbation-based testing framework for scalable distributed systems.
Proceedings of the First ACM SIGOPS Conference on Timely Results in Operating Systems, 2013

Feedback-directed unit test generation for C/C++ using concolic execution.
Proceedings of the 35th International Conference on Software Engineering, 2013

2012
Introduction to special section on verification challenges in the concurrent world.
ACM Trans. Design Autom. Electr. Syst., 2012

Donut Domains: Efficient Non-convex Domains for Abstract Interpretation.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2012

DTAM: dynamic taint analysis of multi-threaded programs for relevancy.
Proceedings of the 20th ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE-20), 2012

Efficient Probabilistic Model Checking of Systems with Ranged Probabilities.
Proceedings of the Reachability Problems - 6th International Workshop, 2012

Efficient predictive analysis for detecting nondeterminism in multi-threaded programs.
Proceedings of the Formal Methods in Computer-Aided Design, 2012

Symbolic Trajectory Evaluation: The primary validation Vehicle for next generation Intel® Processor Graphics FPU.
Proceedings of the Formal Methods in Computer-Aided Design, 2012

Object Model Construction for Inheritance in C++ and Its Applications to Program Analysis.
Proceedings of the Compiler Construction - 21st International Conference, 2012

Concurrent Test Generation Using Concolic Multi-trace Analysis.
Proceedings of the Programming Languages and Systems - 10th Asian Symposium, 2012

2011
Symbolic predictive analysis for concurrent programs.
Formal Aspects Comput., 2011

Predictive analysis for detecting serializability violations through Trace Segmentation.
Proceedings of the 9th IEEE/ACM International Conference on Formal Methods and Models for Codesign, 2011

DC2: A framework for scalable, scope-bounded software verification.
Proceedings of the 26th IEEE/ACM International Conference on Automated Software Engineering (ASE 2011), 2011

BEST: A symbolic testing tool for predicting multi-threaded program failures.
Proceedings of the 26th IEEE/ACM International Conference on Automated Software Engineering (ASE 2011), 2011

Coverage guided systematic concurrency testing.
Proceedings of the 33rd International Conference on Software Engineering, 2011

Predicting Serializability Violations: SMT-Based Search vs. DPOR-Based Search.
Proceedings of the Hardware and Software: Verification and Testing, 2011

Modeling and Analyzing the Interaction of C and C++ Strings.
Proceedings of the Formal Verification of Object-Oriented Software, 2011

Verifying concurrent programs: <i>tutorial talk</i>.
Proceedings of the International Conference on Formal Methods in Computer-Aided Design, 2011

Interprocedural Exception Analysis for C++.
Proceedings of the ECOOP 2011 - Object-Oriented Programming, 2011

2010
Trace-Based Symbolic Analysis for Atomicity Violations.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2010

Program analysis via satisfiability modulo path programs.
Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2010

Numerical stability analysis of floating-point computations using software model checking.
Proceedings of the 8th ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2010), 2010

Monte-carlo techniques for falsification of temporal properties of non-linear hybrid systems.
Proceedings of the 13th ACM International Conference on Hybrid Systems: Computation and Control, 2010

Integrating ICP and LRA solvers for deciding nonlinear real arithmetic problems.
Proceedings of 10th International Conference on Formal Methods in Computer-Aided Design, 2010

Scalable and precise program analysis at NEC.
Proceedings of 10th International Conference on Formal Methods in Computer-Aided Design, 2010

2009
Model checking sequential software programs via mixed symbolic analysis.
ACM Trans. Design Autom. Electr. Syst., 2009

Preface.
Formal Methods Syst. Des., 2009

Model Checking Concurrent Programs.
Proceedings of the Verification, 2009

Semantic Reduction of Thread Interleavings in Concurrent Programs.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2009

Symbolic pruning of concurrent program executions.
Proceedings of the 7th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2009

Robustness of Model-Based Simulations.
Proceedings of the 30th IEEE Real-Time Systems Symposium, 2009

Symbolic Predictive Analysis for Concurrent Programs.
Proceedings of the FM 2009: Formal Methods, 2009

Refining the control structure of loops using static analysis.
Proceedings of the 9th ACM & IEEE International conference on Embedded software, 2009

Monotonic Partial Order Reduction: An Optimal Symbolic Partial Order Reduction Technique.
Proceedings of the Computer Aided Verification, 21st International Conference, 2009

2008
Efficient SAT-based bounded model checking for software verification.
Theor. Comput. Sci., 2008

Bitwidth Reduction via Symbolic Interval Analysis for Software Model Checking.
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2008

Peephole Partial Order Reduction.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2008

Efficient Modeling of Concurrent Systems in BMC.
Proceedings of the Model Checking Software, 2008

Modular verification of web services using efficient symbolic encoding and summarization.
Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2008

SLR: Path-Sensitive Analysis through Infeasible-Path Detection and Syntactic Language Refinement.
Proceedings of the Static Analysis, 15th International Symposium, 2008

Dynamic inference of likely data preconditions over predicates by tree learning.
Proceedings of the ACM/SIGSOFT International Symposium on Software Testing and Analysis, 2008

Mining library specifications using inductive logic programming.
Proceedings of the 30th International Conference on Software Engineering (ICSE 2008), 2008

Completeness in SMT-based BMC for Software Programs.
Proceedings of the Design, Automation and Test in Europe, 2008

Tunneling and slicing: towards scalable BMC.
Proceedings of the 45th Design Automation Conference, 2008

Software Verification: Roles and Challenges for Automatic Decision Procedures.
Proceedings of the Automated Reasoning, 4th International Joint Conference, 2008

Dynamic Model Checking with Property Driven Pruning to Detect Race Conditions.
Proceedings of the Automated Technology for Verification and Analysis, 2008

2007
SAT-Based Scalable Formal Verification Solutions
Series on Integrated Circuits and Systems, Springer, ISBN: 978-0-387-69167-1, 2007

Disjunctive image computation for software verification.
ACM Trans. Design Autom. Electr. Syst., 2007

SDSAT: Tight Integration of Small Domain Encoding and Lazy Approaches in Solving Difference Logic.
J. Satisf. Boolean Model. Comput., 2007

Synthesizing "Verification Aware" Models: Why and How?
Proceedings of the 20th International Conference on VLSI Design (VLSI Design 2007), 2007

Program Analysis Using Symbolic Ranges.
Proceedings of the Static Analysis, 14th International Symposium, 2007

On the analysis of interacting pushdown systems.
Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2007

Using Ontologies and the Web to Learn Lexical Semantics.
Proceedings of the IJCAI 2007, 2007

Hybrid CEGAR: combining variable hiding and predicate abstraction.
Proceedings of the 2007 International Conference on Computer-Aided Design, 2007

From Hardware Verification to Software Verification: Re-use and Re-learn.
Proceedings of the Hardware and Software: Verification and Testing, 2007

Induction in CEGAR for Detecting Counterexamples.
Proceedings of the Formal Methods in Computer-Aided Design, 7th International Conference, 2007

Using Counterexamples for Improving the Precision of Reachability Computation with Polyhedra.
Proceedings of the Computer Aided Verification, 19th International Conference, 2007

Fast and Accurate Static Data-Race Detection for Concurrent Programs.
Proceedings of the Computer Aided Verification, 19th International Conference, 2007

Efficient BMC for Multi-Clock Systems with Clocked Specifications.
Proceedings of the 12th Conference on Asia South Pacific Design Automation, 2007

2006
Efficient distributed SAT and SAT-based distributed Bounded Model Checking.
Int. J. Softw. Tools Technol. Transf., 2006

<i>SDSAT</i>: Tight Integration of <i>Small Domain Encoding</i> and <i>Lazy</i> Approaches in a Separation Logic Solver.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2006

SAT-Based Verification Methods and Applications in Hardware Verification.
Proceedings of the Formal Methods for Hardware Verification, 2006

Static Analysis in Disjunctive Numerical Domains.
Proceedings of the Static Analysis, 13th International Symposium, 2006

Mixed symbolic representations for model checking software programs.
Proceedings of the 4th ACM & IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE 2006), 2006

An Automata-Theoretic Approach for Model Checking Threads for LTL Propert.
Proceedings of the 21th IEEE Symposium on Logic in Computer Science (LICS 2006), 2006

Accelerating high-level bounded model checking.
Proceedings of the 2006 International Conference on Computer-Aided Design, 2006

Disjunctive image computation for embedded software verification.
Proceedings of the Conference on Design, Automation and Test in Europe, 2006

Predicate learning and selective theory deduction for a difference logic solver.
Proceedings of the 43rd Design Automation Conference, 2006

Symbolic Model Checking of Concurrent Programs Using Partial Orders and On-the-Fly Transactions.
Proceedings of the Computer Aided Verification, 18th International Conference, 2006

Using Statically Computed Invariants Inside the Predicate Abstraction and Refinement Loop.
Proceedings of the Computer Aided Verification, 18th International Conference, 2006

Whodunit? Causal Analysis for Counterexamples.
Proceedings of the Automated Technology for Verification and Analysis, 2006

2005
Verification Languages.
Proceedings of the Embedded Systems Handbook., 2005

A survey of recent advances in SAT-based formal verification.
Int. J. Softw. Tools Technol. Transf., 2005

Lazy Constraints and SAT Heuristics for Proof-Based Abstraction.
Proceedings of the 18th International Conference on VLSI Design (VLSI Design 2005), 2005

Localization and Register Sharing for Predicate Abstraction.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2005

<i>DiVer</i>: SAT-Based Model Checking Platform for Verifying Large Scale Systems.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2005

Deciding Separation Logic Formulae by SAT and Incremental Negative Cycle Elimination.
Proceedings of the Logic for Programming, 2005

Model Checking C Programs Using F-SOFT.
Proceedings of the 23rd International Conference on Computer Design (ICCD 2005), 2005

Verification of Embedded Memory Systems using Efficient Memory Modeling.
Proceedings of the 2005 Design, 2005

Beyond safety: customized SAT-based model checking.
Proceedings of the 42nd Design Automation Conference, 2005

Symmetry Reduction in SAT-Based Model Checking.
Proceedings of the Computer Aided Verification, 17th International Conference, 2005

Reasoning About Threads Communicating via Locks.
Proceedings of the Computer Aided Verification, 17th International Conference, 2005

F-Soft: Software Verification Platform.
Proceedings of the Computer Aided Verification, 17th International Conference, 2005

Verification Languages.
Proceedings of the Industrial Information Technology Handbook, 2005

2004
Efficient SAT-based unbounded symbolic model checking using circuit cofactoring.
Proceedings of the 2004 International Conference on Computer-Aided Design, 2004

Efficient Modeling of Embedded Memories in Bounded Model Checking.
Proceedings of the Computer Aided Verification, 16th International Conference, 2004

2003
Iterative Abstraction using SAT-based BMC with Proof Analysis.
Proceedings of the 2003 International Conference on Computer-Aided Design, 2003

Learning from BDDs in SAT-based bounded model checking.
Proceedings of the 40th Design Automation Conference, 2003

Abstraction and BDDs Complement SAT-Based BMC in DiVer.
Proceedings of the Computer Aided Verification, 15th International Conference, 2003

2002
Assertion-based verification turns the corner.
IEEE Des. Test Comput., 2002

Property-Specific Testbench Generation for Guided Simulation.
Proceedings of the 7th Asia and South Pacific Design Automation Conference (ASP-DAC 2002), 2002

Combining strengths of circuit-based and CNF-based algorithms for a high-performance SAT solver.
Proceedings of the 39th Design Automation Conference, 2002

2001
Using complete-1-distinguishability for FSM equivalence checking.
ACM Trans. Design Autom. Electr. Syst., 2001

Partition-Based Decision Heuristics for Image Computation Using SAT and BDDs.
Proceedings of the 2001 IEEE/ACM International Conference on Computer-Aided Design, 2001

Property-specific witness graph generation for guided simulation.
Proceedings of the Conference on Design, Automation and Test in Europe, 2001

Dynamic Detection and Removal of Inactive Clauses in SAT with Application in Image Computation.
Proceedings of the 38th Design Automation Conference, 2001

2000
Fast Error Diagnosis for Combinational Verification.
Proceedings of the 13th International Conference on VLSI Design (VLSI Design 2000), 2000

SAT-Based Image Computation with Application in Reachability Analysis.
Proceedings of the Formal Methods in Computer-Aided Design, Third International Conference, 2000

1999
Verification of Scheduling in the Presence of Loops Using Uninterpreted Symbolic Simulation.
Proceedings of the IEEE International Conference On Computer Design, 1999

Exploiting Retiming in a Guided Simulation Based Validation Methodology.
Proceedings of the Correct Hardware Design and Verification Methods, 1999

1998
Integrating a Boolean Satisfiability Checker and BDDs for Combinational Equivalence Checking.
Proceedings of the 11th International Conference on VLSI Design (VLSI Design 1991), 1998

1997
Toward Formalizing a Validation Methodology Using Simulation Coverage.
Proceedings of the 34st Conference on Design Automation, 1997

1994
Tradeoffs in Canonical Sequential Function Representations.
Proceedings of the Proceedings 1994 IEEE International Conference on Computer Design: VLSI in Computer & Processors, 1994

1993
Representation and symbolic manipulation of linearly inductive Boolean functions.
Proceedings of the 1993 IEEE/ACM International Conference on Computer-Aided Design, 1993

Parametric Circuit Representation Using Inductive Boolean Functions.
Proceedings of the Computer Aided Verification, 5th International Conference, 1993

1992
Formal Hardware Verification Methods: A Survey.
Formal Methods Syst. Des., 1992

1990
Flexible Parallel Polygon Rendering.
Proceedings of the 1990 International Conference on Parallel Processing, 1990

1986
A Parallel Computer Based on Cube-Connected Cycles for Wafer-Scale.
Proceedings of the Fall Joint Computer Conference, November 2-6, 1986, Dallas, Texas, USA, 1986


  Loading...