We have implemented a new method for eliminating reference parameter aliases. This method allows procedure calls with overlapping call-by-reference parameters, but at the same time guarantees that procedure bodies are alias-free. The method involves writing multiple bodies for a procedure: one per aliasing combination. Calls are automatically dispatched to the appropriate procedure body based on the particular alias combination among the actual parameters and imported global variables. This makes writing verifiable client code simpler, since such code does not need to determine the aliasing combination before the procedure is called. The efficiency of dispatch to these bodies is no worse than hand-coded determination of the aliasing combination would be in other languages. In our experience, the number of necessary procedure bodies is usually small, which makes the approach practical. Forcing programmers to write one body for each aliasing combination also makes them consider each case of aliasing among the parameters and globals, making it more likely that the procedure is correctly implemented.